Proof theory and computer science are jointly engaged in a remarkable enterprise. Together they provide the practical means to formalize vast amounts of mathematical knowledge. They have created the subject of automated reasoning and a digital computer based proof technology; these enable a diverse community of mathematicians, computer scientists, and educators to build a new artifact -- a globally distributed digital library of formalized mathematics. I think that this artifact signals the emergence of a new branch of mathematics, perhaps to be called Formal Mathematics.
The theorems of this mathematics are completely formal and are processed digitally. They can be displayed as beautifully and legibly as journal quality mathematical text. At the heart of this library are completely formal proofs -- created with computer assistance. Their correctness is based on the axioms and rules of various foundational theories; this formal accounting of correctness supports the highest known standards of rigor and truth. The need to formally relate results in different foundational theories opens a new topic in proof theory and foundations of mathematics.
Formal proofs of interesting theorems in current foundational theories are very large rigid objects. Creating them requires the speed and memory capacities of modern computer hardware and the expressiveness of modern software. Programs called theorem provers fill in tedious detail; they recognize many kinds of ``obvious inference,'' and they automatically find long chains of inferences and even complete subproofs or proofs. The study of these theorem provers and the symbolic algorithms that make them work is part of the subject of automated reasoning. This science and the proof technology built on it are advancing all the time, and the new branch of mathematics that they enable will have its own standards, methods, surprises and triumphs.
This article is about the potent mixture of proof theory and computer science behind automated reasoning and proof technology. The emphasis is on proof theory topics while stressing connections to computer science.
Computer science is concerned with automating computation. Doing this well has made it possible to formalize real proofs. Computing well requires fast and robust hardware as well as expressive high level programming languages. High level languages are partially characterized by their type systems; i.e., the organization of data types expressible in the language. The evolution of these languages has led to type systems that resemble mathematical type theories or even computationally effective set theories. (This development underlines the fact that high level programming is an aspect of computational mathematics.) This article will focus mainly on relating data types and mathematical types.
The connection between data types and mathematical types in the case of formal mathematics and automated reasoning is even tighter than the general connection. Here is why. To preserve the highest standards of rigor in formalized mathematics built with computer assistance (the only way to produce it), it is necessary to reason about programs and computations. This is what intuitionists and constructivists do at a very high level of abstraction. So as the programming languages for automating reasoning become more abstract and expressive, constructive mathematics becomes directly relevant to Formal Mathematics and to the ``grand enterprise'' of building it using theorem provers. We will see that connections are quite deep.
It turns out that proof technology is relevant to other technologies of economic and strategic importance. For instance, the type checkers in commercial programming languages like ML are actually small theorem provers. They check that arguments to a function match the type of the function (see section 3). Industrial model checkers systematically search for errors in the design of finite state systems, such as hardware circuits or software protocols. More general tools are program verification systems. These combine type checkers, model checkers, decision procedures, and theorem provers that use formalized mathematics. They are employed to prove that programs have certain formally specified properties. Such proofs provide the highest levels of assurance that can be given that programs operate according to specifications. There are also software systems based on proof technology which synthesize correct programs from proofs that specifications are realizable. We will examine the proof theory underlying some of these systems.
My approach to the subject comes from the experience of designing, studying, and using some of the earliest and then some of the most modern of these theorem provers. Currently my colleagues and I at Cornell are working with the system we call Nuprl (``new pearl'').2 We call it a proof development system in [28], but some call it a problem solving environment (PSE) or a logical frameworklogical framework (LF). >From another point of view it is a collaborative mathematics environment, c.f., [23]. Whatever Nuprl is called, I am concerned with systems like it and their evolution. We will examine the logical features common to a variety of current systems of a similar kind, such as ACL2, Alf, Coq, HOL, IMPS, Isabelle, Kiv, LA, Lego, Mizar, NqThm and Otter. [36,43,42,95,91,97]. So while I will refer to Nuprl from time to time, most of the ideas are very general and will apply to the systems of the 21st century as well. Before saying more about the article, let me put the work into historical perspective. Doing this will allow me to state my goals more exactly (especially after each topic of Section 1).