next up previous contents index
Next: This Document Up: Overview Previous: Physical Characteristics

The ``Feel'' of the System

Nuprl is an example of an entity which is more than the sum of its parts. It is more than a proof checker or proof--generating editor. It is more than an evaluator for a rich class of functional expressions and more than a system for writing heuristic procedures to find proofs in a specific foundational theory. The integration of these parts creates a new kind of system. One can sense new possibilities arising from this combination both in the system as it exists now and in its potential for growth.

We find that Nuprl as it runs today serves not only as a new tool for writing programs and program specifications but also as a tool for writing nearly any kind of mathematics. Working in the Nuprl environment results in a distinctive style of mathematics---a readable yet formal algorithmic style. The style in turn suggests new mathematical substance such as our treatment of recursive  types and partial  

functions [Constable & Mendler 85]. Nuprl also offers a coherent way to organize and teach a collection of concepts that are important in computer science.

As we extrapolate the course of Nuprl 's development we see the emergence of a new kind of ``intelligent''  system. The mechanisms for the accumulation of mathematical knowledge in the form of definitions, theorems and proof techniques are already in place, and as more of this knowledge is accumulated the system exhibits a more widely usable brand of formal mathematics. Furthermore, since the tactic mechanism gives the system access to the contents of its libraries, one can envision altering the system so that it generates and stores information about itself. In this sense Nuprl is an embryonic intelligent system.

Richard Eaton
Thu Sep 14 08:45:18 EDT 1995