One of the salient features of
is that the
logic and the system take account of the
computational meaning
of assertions and proofs. For instance, given
a constructive existence proof the
system can use the computational information in the proof to build
a representation of the object which demonstrates the truth of the
assertion.
Such proofs can thus be used to provide data for further
computation or display. Moreover,
a proof that for any object x of type A we can build an object y of
type B satisfying relation 
implicitly defines a computable
function f from A to B. The system can build f from the proof, and it can evaluate f on inputs of type A. For example, given any mapping f of a nonempty set A onto a finite set B of smaller but nonzero cardinality, one can say that there will be two points of A mapped to the same point of B. From a proof of this statement the system can extract a function which given specific A, B and f produces two points of A mapped to the same point of B. This function expresses the computational content of the theorem and can be evaluated.
As a computer system supports an interactive environment for text editing, proof generation and function evaluation. The interaction is oriented around a computer terminal with a screen and a mouse , for our intention is to provide a medium for doing mathematics different from that provided by paper and blackboard. Eventually such a medium may support a variety of input devices and may provide communication with other users and systems; the essential point, however, is that this new medium is active, whereas paper, for example, is not. This enables the interactive style of proof checking that characterizes Nuprl ; in this system it is impossible to develop an incorrect proof.
also possesses some of the characteristics of an intelligent computer system in that it provides its users with a facility for writing proof--generating programs in a metalanguage, ML. The implementation of the logic codes into Nuprl certain primitive mathematical knowledge in the form of rules for generating proofs and in the form of certain defined types in ML. As people use Nuprl they create libraries of mathematical facts, definitions and theorems; they can also create libraries of ML programs which use these results and other ML programs to generate proofs of theorems. In a very real sense, as
is used its capacity for providing help in proving theorems increases. By virtue of this property, possesses aspects of an intelligent system.
The system design exhibits several key characteristics.
The style of the logic is based on the stepwise refinement paradigm
for problem solving in that the system encourages the user to work
backward from goals to subgoals until one reaches what is known.
Indeed, the system derives its name, Proof Refinement Logic,
from this method of
presentation.
The logic has a constructive semantics in that
the meaning of propositions is given by rules of use and in terms of computation.
We discuss these features in more
detail later.
In a larger sense the system serves as a tool for experimenting with ways of applying computer power to solving problems and to generating exact explanations of solutions, especially in the realm of computational mathematics. Because the difficult part of computer programming is precisely in problem solving and in explaining algorithmic solutions, we think that a system of this kind will eventually have a lasting impact on our ability to produce reliable and understandable programs.