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.

Thu Sep 14 08:45:18 EDT 1995