Nuprl is a large evolving system. We try to use concepts and principles from Software Engineering to design it, maintain it and control its evolution and reliability. We have set ourselves the goal to use the Formal Methods tools that we have built in our own work and to bring to bear more and more of our own system components in the process of managing Nuprl itself.
Joe Bates was the first lead architect for the PRL systems, and he established traditions that still influence our practices. One tradition is that we write down designs and talk about them in the PRL seminar. Another is that key designs are discussed with project members. Joe was keen on keeping records of these discussions that included definitions of the basic components and a rationale for design steps. The goal was to produce an error free system in a style that documented the design.
Another key goal that determined our early practice is that the system would be built by a team of programmers including graduate students. Student involvement is a continuous source of fresh ideas, new perspectives, and new energy. Also, explaining the existing code to students helps keep it clean, documented, and rationalized. To facilitate student involvement, we conduct weekly seminars. In addition there are less regular staff meetings in which system design and goals are discussed. (For Nuprl 3 these staff meetings were also weekly.)
The original PRL system was designed as six main modules: the library; the evaluator; the metalanguage; the refiner; the text editor (ted); and the refinement editor (red). It was coded in Common Lisp on Lisp machines. The LambdaPRL system was the prototype for Nuprl. The idea was to modify that architecture for the new system.
The choice of programming language was a major decision. Lisp was seen as the standard language for automated reasoning research, and we felt that supporting tools would tend to be written in Lisp. We expected to interface with AI tools such as knowledge representation languages and planners, and we expected to gain significant productivity from the Lisp machine's integrated programming environment. (The old timers claim that we have not seen such a good environment since then.)
The choice of Lisp also reflects one of the key practices that we admire and strive to follow, but which is hard to implement. It is the idea of sharing code and designs with other research groups. Our first major step in this direction was taking up the Cambridge ML tactic mechanism and modifying it to suit Nuprl. This was a major success. Another success was Pavel Naumov's use of the Web to present Nuprl proofs. Another major success along these lines is Doug Howe's link to HOL libraries. We plan to build further on these successes.
There have been notable failures in attempting to import other technology and interface with other groups. We have tried three times to link with Tim Teitelbaum's Synthesizer Generator to provide a standard and alternative front end to Nuprl. We have spent a considerable amount of time and dollars on this effort with only a small prototype term editor to show for it. We also have been unable to import data base technology - either from AI knowledge bases or standard data bases.
We tried hard to incorporate the Weyl computer algebra system, also written in Common Lisp. But we found that Weyl and Nuprl had different ideas about the basic algebraic data types that made cooperation very difficult. We may try this again when we have more experience with the successes.
Nuprl 4 was a significant advance over Nuprl 3, and we learned a great deal about software engineering from making the transition. The major advances from Nuprl 3 to Nuprl 4 were in the term structure, the proof editor and in the tactic collection. The term structure of Nuprl 4 is uniform and more abstract than that of version 3. The uniformity made the code much cleaner and more extensible. It made it possible to reflect the system in itself and it enabled a much more powerful proof editor. One of the key lessons of this design is the power of abstraction. The more abstract the design, the cleaner and more extensible the code.
Nuprl 4 was created by a different process than Nuprl 3. It was done by the professional staff. The chief programmer was Richard Eaton who also designed key components such as the rule compiler. The professional team included Stuart Allen, Doug Howe, Chet Murthy, Richard Eaton and Robert Constable. These were all professors or research associates or staff.
Students and users played a role in evaluating and criticizing the design and there was a long feedback process that led to the current stable and highly reliable version 4.2. Paul Jackson rebuilt the tactic collection on top of the version 4 system and created the first editor. But in the transition from Nuprl 3 to Nuprl 4.0, we made the mistake of not importing all Nuprl 3 libraries, and we forced our user base to convert to Nuprl 4; this caused considerable disruption.
Our experience with the transition to Nuprl 4 caused us to institute a key practice followed by Boyer and Moore from the beginning. They maintain a suite of theorems that must be reproved after every system change, using a "prove all" command. We now maintain such a benchmark library. We measure system performance based on reproving this large library. We also have plans to restore the Nuprl 3 libraries based on the Nuprl 5 Library design.
The experience of having the design team disconnected from the users convinced us that we need a more incremental release path for the next system. We think that new designs should attempt to move component by component if at all possible. The architects and programmers should be getting continuous feedback from the users.
We also learned the lesson that we must keep performance within reasonable bounds. Even though hardware speeds have kept the project optimistically expanding and have allowed us to postpone major "performance enhancement projects," nevertheless we know that speed is the one objective criterion we can apply to new designs. We also know that increased processor speeds and larger memories will carry the project into new territory where we can explore higher level assistance in developing proofs and finding proofs. So we now regularly benchmark changes against the old system and try to steadily improve performance.
Nuprl 4 was a significant but still incremental improvement in system design. It left open many issues that we had been studying since the late 80s, and experiments with it brought into view new challenges on the infinite horizon. So we again took up the issues of system design in 1995. We were strongly motivated by two concerns; one was the desire to integrate a modern programming language, a modern ML as the term language of Nuprl. The other was a wish to extend formal support from the design and coding of programs to the design and coding of systems. We also sensed the need for integrating other tools, such as computer algebra systems. Furthermore we realized in talking to colleagues and students that we needed to reopen the system design process to students. Tapping this incredible university resource enabled us to build the PRL systems in the first place. We are already seeing extraordinary benefits from reopening the system design and coding to students. The work of Aleksey Nogin on the Nuprl-Light evaluator is some of the most innovative work on evaluation in the project.
These concerns led to the design of a significantly new system. This process again involved students heavily. We spent over a year considering priorities for a better inference mechanism, for a more open and modular system design, for more efficient structure editing, for a concurrent logic engine, and for a library structure that would allow results from multiple logics. We also considered how to integrate Nuprl and its programming language more tightly and to support a modern programming language, a dialect of ML as the term language of Nuprl. These discussions took place with researchers and students and were presented in the weekly PRL seminar. They were informed by a detailed system critique provided over several months by Chet Murthy who knew both Nuprl 3 and 4 inside and out. We also worked with Tim Teitelbaum so that our open architecture could accommodate external editors and we worked with Richard Zippel to insure that we could interface to symbolic algebra systems like Weyl.
Nuprl-Light is Jason Hickey's response to the architectural issues. His thesis involved a careful study of the problems and goals that he and the group discussed for nearly two years. Nuprl 5 is the new open modular system architecture that will provide the basis for evolution over the next five years. Nuprl-Light will be a detachable component of the Nuprl 5 system.
The key lesson from this period has been the advantages of open modular design. We have also gained greatly from renewing our links to the excellent work being done on the OCaml compiler.
Our system designs have always been strongly informed by the mathematics underlying the PRL systems. Several components and modules of Nuprl can be precisely specified. For example, the data type of terms corresponds almost exactly to the reflected internal recursive data type of terms. The substitution algorithm which is basic to the correct operation can be precisely specified in type theory. The refiner can be defined as a function in type theory. We can give formal semantics to the ML metalanguage as well as the object level terms of Nuprl. The editor is a suite of ML functions operating on terms.
This mathematical basis lies behind the system design, and conversely the system design influences the mathematics. For example, the refiner is a goal directed proof engine. This entails a version of the proof rules of type theory which is top down instead of the usual bottom up format. There are significant mathematical consequences from this decision. As another example, since the refiner can affect the proof editor, there is no sharp boundary between editing and proving.
A verification system is like an accounting system, as Stuart Allen is fond of pointing out. It must account for truth. It does this through proof. The notion of proof depends on the axioms and inference rules and on access to previously proved theorems. The Nuprl design puts axioms, rules and results in the Library. So library management is critical to accounting for truth. Our goal is to build a logical library.
Once we have a sound logical library, it can be used to help maintain the system. It acts like a logic-based version control system. It acts like a code data base as well as a theorem knowledge base.
Formal Methods in Nuprl System Design and ConstructionIt is a fact that some algorithms can be precisely defined has been used in coding the system. For instance, the substitution algorithm was written first by Allen as an ML program about which we could informally prove key properties. This ML code is our reference algorithm for the system code.
Our work on reflection has provided a mathematical definition of the term structure and logic engine. This is a formal template against which to compare the system code for these components.