User Interfaces to Proof Assistants

The field of human-computer interaction (HCI) has grown rapidly along with the lowering cost of computers (especially personal computers). The cost of computer hardware now pales in comparison to the cost of employing its users. Non-expert users are far more common than experts. User centered design processes can open the use of computer applications to a much wider group of people than machine-centred designs.

Perhaps the best claim to the need for graphical user interfaces to proof assistants was made by Théry, Bertot and Kahn in [55]. Their view is that finding proofs may one day become a routine part of a software engineer's job. In order to convince these users that the use of proofs is viable, the cost of producing these proofs should be dwarfed by the value of the proof. Users are resistant to change, so a large amount of work should be put into making the system as appealing to the user as possible.

Since this paper, it appears that the design of user interfaces to theorem proving has taken the recommended path of separating the interface from the proof engine. The two most interesting proof assistants in active development are Proof General [5], implemented in Emacs Lisp (see [21])Emacs is a text editor based upon an interpreter of a dialect of Lisp known as Emacs Lisp (``elisp'' for short). and capable of being used with multiple different proof assistants, and Pcoq [4], implemented in Java for use with Coq [10]. Both are distinct entities from the proof engine. These are the primary two interfaces I plan to borrow ideas from.