tools for the classroom We know that it is possible to use the latest technology in teaching, for example, Macsyma was available to undergraduates at MIT on Multics already in the 70's, and Mathematica [81] and Matlab are now widely used. CAD tools are used in hardware courses and so on. In modern computer science we see comprehensive programming environments used in the classroom; it would even be possible to use program verification tools.
Essentially we are proposing to gradually move a high-powered research tool, Nuprl, into the classroom. The first steps are possible because of the Web and because PC's under Linux and Sun's under Solaris can run Nuprl for people willing to install it. Also, more functionality of Nuprl will be made available via the Web over the next eighteen months. Underlying the use is a close alignment between the aims of the research and the needs in the classroom. The devices we have built for our Formal Methods research are precisely what is needed to teach mathematics and computing.
emergence of formal mathematics
Another factor influencing this proposal is that there has been a
dramatic rise in the amount of formal mathematical material over the
past decade.
In the 1970's it took several years to
formalize Landau's very small book Grundlagen der Analysis
[49] in Automath. Now we could generate that material in a
matter of weeks. The Mizar project has published twelve volumes
of computer-checked mathematics in its Journal of Formal
Mathematics covering over 300 articles authored by over 66
mathematicians. Nuprl alone is responsible for over 40 article-size
pieces. We are proposing to organize some of this into course
material which can be done in an especially instructive way since
Nuprl generates readable proofs - whereas most other systems accept
or reject conjectures without readable justification (people call
these ``write only proofs'').
role of computer science
It is interesting that computer science and engineering have played
three major roles in enabling the enterprise we describe. It has
produced hardware platforms of sufficient power to do the work. It
has created software systems that accelerate programming productivity
to the point that ambitious systems can be built with small staffs.
It has also re-centered the philosophical debate about the value of
formal mathematics. By generating large software systems governed
completely by formal rules, it has changed a philosophical question.
At the beginning of the century, in response to Hilbert's program it
was, ``Can formalism explain and justify mathematical practice?'' Now
at the end of the century it is, ``How can we use mathematics to
explain and control the monumental amount of useful formal
material (including the mathematical) that will be a large factor of
the human condition in the 21st century?''
We are proposing to capitalize on the existence of this new artifact by bringing it into the classroom. This will enable us to teach mathematics, computing, and their applications in science and engineering in new ways. But it will also teach a lesson unique to our times. We can demonstrate a new kind of knowledge in which explanation is completely precise and rests ultimately on only explicit assumptions in a way we can track.