One of the most interesting features of the Nuprl logic is that it supports computational reasoning as well as classical. In order to do that there must be a programming language implicit in the logic [22][9]. In fact, the notations for computable functions make this language explicit. This enables us to deal with computational problems and issues for any mathematical concept.
The built-in programming language is essentially a subset of ML
[56][34] which can be used to animate constructions and
proofs. For example, the proof that the gcd, say , of two
co-prime numbers
and
is a linear combination of
and
,
say
provides a function,
, to compute
and
from
and
. This computation can be done in-line as
part of a lesson. We say that
is extracted from the proof.
Students find it very appealing to see these proofs come to
life.
The animation of proofs and the extraction of programs from them enables us to connect the mathematical notion of induction to the programming notion of recursion. We exploit this frequently. It illustrates the general principle that the formal connections between objects help teach the abstract links between concepts which appears to be a basic mechanism driving learning.