From the very beginning we imagined the PRL systems as creating a new medium for mathematical problem solving in which paper was replaced by interfaces to the digital medium. We designed the PRL systems from the beginning to work with windows and a mouse. Now these concerns are part of a large field. We try to situate our work in this field.
The name of this field tells us generally what it is about. The fact that one of the pioneers of the field, Doug Englebart, won the Turing Award in 1997 will help make the history of the field more widely known. Englebart is credited with inventing the idea of the mouse and the point-and-click interface to computers that was developed at Xerox Parc and commercialized by Jobs and Wozniak at Apple. The technology has been adopted by Microsoft and has become the PC standard, known to millions. The term GUI (Graphical Unser Interface) also suggests what the field is about.
When the PRL project started in 1979, there were no window packages available. Joe Bates understood the power of this interface for a program development system, so he and Fran Corrado, our first programmer, designed and built a mouse and window interface to PRL in Lisp.
Another key component of modern computer interface systems is the structure editor. We learned of this through Tim Teitelbaum's work at Cornell on the Cornell Program Synthesizer and its successor, the Synthesizer Generator. This system was being developed by Tim for the Terak personal computers just before we designed PRL. This editing style so impressed Bates and Constable that it has been a key part of the PRL user interface ever since. This editing technology has been significantly advanced by Stuart Allen and Richard Eaton who built the Nuprl 4 resident structure editor that is the standard interface for Nuprl.
Bates' technical contributions were embedded in the Nuprl 3 code and acknowledged in the banner that comes up with the system but they have not been published. Allen's and Eaton's contributions are also in the Nuprl code and relatively unpublished as yet. The Nuprl reference manual by Paul Jackson describes a particular editing style which is built on Allen and Eaton's primitives. Allen's new resident editor contains an embedded tutorial and his publication describe some of its features.
The user interface to Nuprl shows a deep side to the potential of HCI. We see that the "intelligence" of the theorem prover can be tightly integrated into the interactions with the user. It is as if the very medium of communication is "alive." One has to try it to understand it.