Powerful User Interfaces for Interactive Theorem Proving

University Of Iowa, Iowa City IA

Investigators

Abstract

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.