UC Santa Cruz
- Author(s): Schuster, Christopher
- Advisor(s): Flanagan, Cormac
- et al.
This dissertation includes contributions to both live programming and program verification and explores how programming environments can be designed to leverage benefits of both concepts in an integrated way.
Programming environments assist users in both writing program code and understanding program behavior. A fast feedback loop can significantly improve this process. In particular, live programming provides continuous feedback for live code updates of running programs. This idea can also be applied to program verification. In general, verifiers statically check programs based on source code annotations such as invariants, pre- and postconditions. However, verification errors are often hard to understand, so programming environment integration is crucial for supporting the development process.
The resulting systems represent possible solutions in a vast design space with various contributions. The research on live programming showed that a programming model that separates event handling from output rendering enables not only live code updates but also runtime version control and programming-by-example. For program verification, esverify represents a novel approach for static verification of both higher-order functional programs and dynamically-typed programming idioms. esverify can verify nontrivial algorithms such as MergeSort and a formal proof in the Lean theorem prover shows that its verification rules are sound. Finally, a programming environment based on esverify supports inspection and live edits of verification conditions including step-by-step debugging of automatically generated tests that serve as executable counterexamples. As part of a user study, participants used these features effectively to solve programming tasks and generally found them to be helpful or potentially helpful.