Software's increasing role in aviation, medical devices, and other safety- and mission-critical tasks is driving a major research effort in software verification, in both academia and industry. This effort involves proving, using formal mathematical methods, that software does what its authors intend it to do. Interactive theorem provers (ITPs) are a key tool in software verification, enabling users to create complex proofs of deep properties beyond the reach of automated provers. In spite of the increasing need for their use, ITPs have limited user interfaces that have hardly evolved in the past 20 years. This makes it difficult for novices to begin using these tools, and limits the productivity of experts. The objective of this research is to design, develop, and evaluate powerful user interfaces for ITPs. The resulting user interfaces will be made freely available to the public as open-source code.
The hypothesis is that a novel ITP user interface that addresses ITP users' information needs through advanced editing techniques will enable novices to prove theorems and understand proofs more quickly and accurately than current ITP user interfaces, and increase productivity for experienced users. Advanced editing techniques will include inference rule and complex syntax visualization and manipulation, as well as proof previews. Together, these techniques will enable users to understand how proofs evolve, more easily read complex formulas, and quickly explore ways of advancing a proof. The hypothesis will be tested using Coq, a widely adopted ITP. The evaluation of the advanced editing techniques will include a comparison with a widely used ITP user interface in terms of efficiency for completing and understanding proofs. Successfully applying modern human-computer interaction techniques to interactive theorem provers will result in a major step forward in the usability and applicability of ITPs. This in turn will help facilitate the increased use of formal methods and verification in academic research, but also with industrial applications. Likewise, it will provide a useful tool for teaching software verification courses by helping students concentrate on proving theorems instead of focusing their attention on how to interact with software. Project results will be disseminated by submission to venues in human-computer interaction and interactive theorem provers.
Software is increasingly being used in critical systems including avionics and healthcare devices. In such systems, mistakes in software implementation could cost lives. While extensive testing can help, the only way to guarantee that these systems are mistake-free is to develop mathematical proofs that the implementations are correct. The most advanced tools for developing these proofs are called interactive theorem provers. They enable computer scientists to prove that software implementations are correct, and can also be used in other fields where mathematical proofs are used, such as mathematics and physics. One of the main barriers to having more software proved to be implemented correctly is that interactive theorem provers are difficult to use. This makes it an expensive activity, both because there are few people who are able to use interactive theorem provers, and because even if they are experts, most proofs can take a significant amount of time to develop. Through this grant, we developed novel user interfaces intended to help novices more quickly get up-to-speed with interactive theorem provers, and experts be more efficient. In terms of software for novices, we developed open source plug-ins for the free cross-platform integrated development environment JEdit. In an evaluation with novice users we found that our novel user interfaces enabled them to complete proofs more quickly, and better interpret existing proofs when compared to a standard user interface for a widely used interactive theorem prover. We also developed a novel user interface to help experts learn keyboard shortcuts, something that can increase efficiency when using text-based user interfaces, such as interactive theorem provers, and integrated development environments for software development. Our innovation, Keyboard-Card Menus, visually displays shortcuts mapped onto a keyboard on the screen, taking advantage of the large displays currently available. In an evaluation we conducted, users were able to learn shortcuts more quickly when using Keyboard-Card Menus than when using standard pull-down menus.
