Skip to main content
eScholarship
Open Access Publications from the University of California

Towards Live Programming Environments for Statically Verified JavaScript

  • Author(s): Schuster, Christopher
  • Advisor(s): Flanagan, Cormac
  • et al.
Creative Commons 'BY' version 4.0 license
Abstract

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 research for this dissertation involved the implementation of esverify, a program verifier for JavaScript, as well as prototype implementations of multiple programming environments. These implementations demonstrate potential benefits and limitations of proposed solutions and enable empirical evaluation with case and user studies. Additionally, the proposed designs were formally defined in order to explain the core idea in a concise way and to prove properties independent of concrete specifics of existing systems and programming languages.

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.

Main Content
Current View