Thoughts on user interfaces for theorem provers

> Actual interaction with LCF and its descendants such as HOL involved the crudest possible user interface: a split Emacs window with the top pane containing the proof being developed and the bottom pane a UNIX shell running the theorem prover. People wrote Emacs macros to streamline the step of copying material from the proof into the prover and executing it. Such habits persisted even after the X Window System became available: I can still remember Mike Gordon allowing a single Emacs window to take up his entire screen (and he liked really big screens). We got a lot of criticism from people who insisted that we should be using WIMP ideas much more. [...] > Proof General, by David Aspinall, is essentially a beefed up version of the Emacs interaction model outlined above. The top pane holds a proof script while the bottom pane holds a running prover process. The user can step through the proof script by clicking repeatedly on the “forward” button; the cursor indicates the current location in the proof, which is actually executed below. Crucially, there is also a “back” button, through which any step (including declarations) can be undone. An internal protocol communicates between Proof General and the prover. Access to other prover features can also be provided through menus.