Mechanizing Proof: Computing, Risk, and Trust. Donald MacKenzie. xii + 427 pp. The MIT Press. 2001. $45.
Among all mechanical contrivances, the digital computer seems closest to the deterministic world of mathematics and logic. Indeed, the components of computer circuits are called logic gates. Their operation should be completely predictable. But anyone who has ever taken mouse in hand knows that computers are the most failure-prone, fickle and unpredictable machines we meet in daily life. (No one ever has to reboot a refrigerator.)
Donald MacKenzie's Mechanizing Proof illuminates this curious situation by exploring the concept of proof as it is understood both in mathematics and in computer science. These two disciplines—or cultures—are closely related and yet sometimes estranged. The idea of proof turns out to be a crucial meeting ground between them, where similarities and differences come into sharp focus.
MacKenzie's story has two mirror-image aspects. On the one hand, computers can help construct proofs in mathematics; on the other, proof techniques borrowed from mathematics might help in constructing correct computer programs.
The pioneer among programs for creating mathematical proofs was the Logic Theory Machine of Herbert Simon and Allen Newell, which proved its first theorem in 1956. (The theorem, hardly an earthshaking novelty, states that if a proposition implies its own negation, then the proposition must be false.) Most of the proof-building programs were intended to assist human mathematicians—or else be assisted by them—but at least one intrepid program was set loose to explore basic mathematics on its own. That program, written by Douglas Lenat, started out with some elementary concepts in set theory and logic; Lenat reported that the program independently discovered the idea of numbers and even went on to conjecture the fundamental theorem of arithmetic (that every number can be factored into primes in just one way). The claims of independent discovery were not universally accepted.
The most famous use of a computer in mathematics came in the proof of the four-color theorem, an episode that gets a full chapter in MacKenzie's book. The theorem states that no more than four colors are ever needed on a map where any two countries sharing a boundary line must have different colors. The proof was completed in 1976 by Wolfgang Haken, Kenneth Appel and John Koch with assistance from a computer at the University of Illinois at Urbana-Champaign. The computer was hardly a full intellectual partner in this undertaking; its task was merely to check the properties of some 1,936 specific map configurations. Nevertheless, the proof stirred controversy, and some questioned whether it should be admitted into the literature of mathematics, on the grounds that no (human) mathematician could follow the argument in full detail.
Since the 1970s, controversy over the role of computers in mathematics seems to have died down—but so has much of the enthusiasm. Automated theorem proving has become a small subspecialty within the field of artificial intelligence, which itself is considerably diminished. The major mathematics journals have not been flooded with machine-generated proofs. For more routine tasks, the computer is accepted as just another tool of the trade, not much more exciting than chalk.
The flow of ideas in the opposite direction—applying the methods of mathematical proof to computers and computations—also has a troubled history. The notion seems natural enough: We can prove that the square of the hypotenuse is equal to the sum of the squares of the sides of a right triangle, so why not prove the correctness of a computer program for calculating the hypotenuse? In the 1960s John McCarthy, Edsger W. Dijkstra and others campaigned strenuously for such a rigorous, mathematical approach to programming, and the formal verification of software became a major research topic in computer science. But today proofs of large programs are seldom attempted; instead, most software engineering still relies on cycles of testing and debugging and patching.
Skeptics argue that formal software verification is doomed to fail, because the task is logically impossible. James H. Fetzer wrote in 1988 that applying the concept of proof to software is a "category mistake," because programs exist in the imperfect world of physical objects, not in the mathematical realm of exact knowledge; in other words, programs are empirical rather than empyrean. Whether or not this supposed flaw is truly fatal, it seems somewhat beside the point: In practice, lesser impediments tend to derail software proofs long before such airy philosophical issues ever have a chance to be tested. Here is a simple example of what can go wrong: Although the statements of many programming languages look much like mathematical equations, their semantics can be far more complicated. An innocent-looking program statement such as x = y + 1 is meant to assign a new value to the variable named x, specifically the value of y + 1. The assignment statement appears to do nothing else, but in fact x could refer to the same location in memory as y, with the result that the value of y is altered as well, behind the programmer's back. The need to keep track of all possible interactions of this kind makes a software proof much more tedious and intricate than a typical proof in mathematics.
The obvious way to tame this complexity is to close the loop and recruit the computer itself as an aid in constructing proofs of computer programs. Indeed, yet another twist is to ask the prover program to prove itself correct. This is a dream that has not been abandoned, but it hasn't been achieved yet either. MacKenzie reports that a proof program called ACL2 is at work on proving the correctness of its own implementation.
MacKenzie is a sociologist, which may seem an unlikely calling for someone writing about mathematical proof. There is an explanation: A central question about proof, which comes up over and over in this narrative, is whether it should be viewed as a formal exercise in deductive logic, or whether it is really just a social process by which people reach consensus about what is true. MacKenzie is not at all dogmatic about the answer, and he allows both sides to state their case.
Moreover, Mechanizing Proof is not just a book about the sociology of science. Along the way MacKenzie offers a well-informed, nontechnical description of the underlying issues in mathematics and computer science. All of the appropriate literature has been consulted, and much additional material comes from dozens of interviews conducted by MacKenzie and his students and colleagues. The book tells lots of stories (starting with the famous occasion when a newly commissioned computer at the North American Air Defense Command mistook the rising moon for a volley of Soviet missiles). The subject is the search for rigor, but the prose is pleasantly informal.—Brian Hayes