Supporting Proof in a Reactive Development Environment ∗

Reactive integrated development environments for soft-ware engineering have lead to an increase in productiv-ity and quality of programs produced. They have done so by replacing the traditional sequential compile, test, debug development cycle with a more integrated and reactive de-velopment environment where these tools are run automat-ically in the background, giving the engineer instant feed-back on his most recent change. The RODIN platform provides a similar reactive devel-opment environment for formal modeling and proof. Using this reactive approach places new challenges on the proof tool used. Since proof obligations are in a constant state of change, proofs in the system must be represented and man-aged to be resilient to these changes. This paper presents a solution to this problem that represents proof attempts in a way that makes them resilient to change and amenable to reuse.