Algorithmic construction

Computer science completely transformed the ``grand enterprise.'' First it introduced computational procedure and procedural knowledge, and it gradually widened the scope of its successes. It could check formulas and synthesize them; later it could check proofs and synthesize them. In all this, the precision that Gödel referred to reached new levels of mechanical precision. The vast change of scale from processing a few hundred lines by hand to tens of thousands by machine (now hundreds of millions) caused a qualitative change and created new fields like Automated Deduction and Formal Mathematics in which formalisms became usable.

The success of procedural knowledge created the questions of relating it to declarative knowledge, a question at the heart of computer science, studied extensively in the database area, also in ``logic programming'' and in AI. It is a question at the heart of AD, [83], as is clearly seen in Bundy's work on proof plans [20]. From the AI perspective, one can see this impact as reintroducing ``mind'' and ``thought'' into the enterprise [83]. From the logical perspective one can see this as reintroducing the study of intension and Frege's notion of sense into logic. As Jean-Yves Girard put it in [50, p.4]:

``In recent years, during which the algebraic tradition has flourished, the syntactic tradition was not of note and would without a doubt have disappeared in one or two more decades, for want of any issue or methodology. The disaster was averted because of computer science -- that great manipulator or syntax -- which posed some very important theoretical problems.''

Computer science produced new high level languages for expressing algorithms. These have evolved to modern programming languages such as ML (for Meta Language) designed to help automate reasoning. ML and its proposed extensions have such a rich system of data types that the type system resembles a constructive theory of mathematical types. We discuss this observation in section 3. Our concern for the relationship between data types and mathematical types is a reason that I will talk so much about typed logic in section 2.

Computer science also created a new medium for doing mathematics -- the digital electronic medium now most visible through the World Wide Web. This affects every aspect of the enterprise. For example, the ``surface'' or concrete syntax can be disconnected from the abstract syntax, and we can display the underlying terms in a large variety of forms. To take a trivial point, the typed universal quantifier, ``for all x of type A'' can be displayed as $\forall x\!:\!A.$ or as $\bigwedge x\!:\!A.$ or as ``For all x in A'' or $\forall x \in A.$ or $\forall x^A:.$ The key parts of the abstraction are the operator name, all, a binding variable, x, and a type, A.

The new medium provides hypertext and hyperproofs, e.g. Nuprl's proof editor and Hyperproof ([6]).⁷ It is difficult to render these proofs on paper as we will see in the appendix; one must ``live in the medium'' to experience it. This medium also creates a new approach to communication and doing mathematics. It is routine to embed computation in documents and proofs, e.g. Mathematica notebooks, [119]. Databases of definitions, conjectures, theorems, and proofs will be available on line as digital mathematics libraries. There will be new tools for collaborating remotely on proofs as we can now do on documents (with OLE, OpenDoc, and similar tools).

These are the overt changes brought by computer science, but as Girard says, the theoretical questions raised are very important to logic.

This article will introduce some of the theory behind tactic-oriented theorem proving and will show examples of modern synthesized proofs. It will relate this to developments in typed programming languages.