User Interface Design in the HolPy Theorem Prover (Invited Talk)

Abstract

HolPy is a new interactive theorem prover implemented in Python. It is designed to achieve a small trusted-code-base with externally checkable proofs, writing proof automation using a Python API, and permit a wide variety of user interfaces for different application scenarios.
In this talk, I will focus on the design of user interfaces in HolPy. While most interactive theorem provers today use text-based user interfaces, there have been several existing work aiming to build point-and-click interfaces where the user perform actions by clicking on part of the goal or choosing from a menu. In our work, we incorporate into the design extensive proof automation and heuristic suggestion mechanisms, allowing construction of proofs on a large scale using this method. We demonstrate the approach in two common scenarios: general-purpose theorem proving and symbolic computation in mathematics.