Thus far, formalized mathematics seems an unpromising idea. Bourbaki may be right that such formalization is simply impractical for people to do. In any case, as [naur-pvf] points out, formalization sometimes leads to more errors, not fewer, as the underlying intuition which provides a check on correctness begins to get lost --- so even one of the claimed merits of formalization is open to question. The problems of formalization have been well put by [constable-programs]:

It is thus possible to translate the proof of any mathematical theorem into a completely formal proof. However, the prospect of actually doing this is quite daunting because an informal proof of modest length will expand to a formal one of prodigious size and will require in its production extreme care and detailed knowledge of the more or less arbitrary conventions of the particular formalism. These tedious details will in sheer number dominate the interesting mathematical ideas which are the raison d'être of the proof.

But like the authors just quoted, we believe that the arrival of the computer changes the situation completely, for several reasons.

1. As pointed out by Naur and others like [vangasteren-shape], as one relies less on intuition and more on rules of formal manipulation, accuracy in those manipulations becomes more important. This is tedious for people,¹⁷ but checking conformance to formal rules is one of the things computers are very good at. Indeed, the Bourbaki claim that the transition to a completely formal text is routine, but too boring and tedious for people, seems almost an open invitation to give the task to computers.

2. The computer need not simply check the correctness of formal arguments, but can try to help in their construction. We will discuss in more detail later how this is to be done, but at one extreme, it is sometimes possible for computers to find proofs of theorems completely automatically. Furthermore, the computer can provide interface assistance, helping to mitigate the austerity of formal deductive calculi and to organize the user's work.

3. Among modern computer scientists, formal logic is quite widely known and substantially used; many regard formal logic as the 'applied mathematics' underlying computer science, just as real analysis etc. underlies physics and engineering. [dijkstra-invariance] has remarked that 'computing scientists may well have been the first to use the predicate calculus regularly [...] as far as the mathematical community is concerned George Boole has lived in vain'.

4. Computer correctness is itself a topic of concern, especially since computers are used in safety-critical systems like fly-by-wire aircraft, antilock braking systems, nuclear reactor controllers and radiation therapy machines. One means of verifying a design is to prove that a mathematical model of the system satisfies some formal properties, designed to correspond to real-world requirements. Such proofs are much more technically intricate, albeit perhaps shallower, than typical mathematics proofs, and of necessity involve very complicated formal manipulations.

It isn't very surprising that the computer should make such a dramatic difference; after all it has revolutionized work in many scientific disciplines. Previously unthinkable ideas like detailed simulations of weather systems have become possible --- formalizing mathematics in a deductive calculus demands fairly modest computer power by comparison.

So thanks to the computer, we may at last be able to do something about the lack of formality in ordinary mathematics. This would be welcome to 'hawkish' logicians¹⁸ like [nidditch], who complained that 'in the whole literature of mathematics there is not a single valid proof in the logical sense', but perhaps not to people such as [demillo-social] who regard the conventional 'social mechanisms of the mathematical community' as the only real means of establishing a valid proof. We do not agree with either of these extreme positions. Regarding the latter, we think that social processes may just be a necessary evil resulting from the difficulty (hitherto) of producing formal proofs.¹⁹ Compare the enthusiasm among the Greeks for deciding scientific questions by a social process rather than empirically, a tendency that survived until about Descartes.

John Harrison 96/8/13; HTML by 96/8/16