In lieu of an abstract, here is a brief excerpt of the content:

Reviewed by:
  • Mechanizing Proof: Computing, Risk, and Trust
  • Steven W. Usselman (bio)
Mechanizing Proof: Computing, Risk, and Trust. By Donald MacKenzie. Cambridge, Mass.: MIT Press, 2001. Pp. xi+427. $45.

This book is first and foremost a significant contribution to the sociology of knowledge. Donald MacKenzie is interested in the nature of proof, the rigorous exercise in deductive knowledge upon which rests the authority of mathematics and formal logic. Sociologists of science have generally neglected [End Page 893] this form of knowledge, notes MacKenzie, concentrating instead upon scientific claims induced from empirical knowledge or asserted authoritatively by certified professional experts.

As his subtitle suggests, MacKenzie frames his inquiry into deductive knowledge with the issues of risk, trust, and the uneasy dependence of "high-modern" societies upon complex computer installations. Many of his introductory sections invoke classic examples, such as false alarms in air defense systems. But MacKenzie does not take us out into those societies to see how groups and individuals perceive matters of risk and trust. Rather, he burrows deep into a community of computer scientists who have since the late 1950s attempted to verify, through rigorous deductive logic, that computer programs would in fact perform as intended. Trust in computing rests ultimately upon these exercises in deductive knowledge, Mackenzie asserts, because we cannot test all possible states of a computer installation (an exercise in induction) and because computer scientists and software engineers have not established strong claims of authority as expert professionals.

MacKenzie traces the emergence and development of program verification through selected case studies of critical watersheds and controversies. Much activity in the field originated in the mid-to-late 1960s. A few influential figures, observing the growing concerns among programmers about the enormous effort and expense incurred in writing and debugging complex software installations, organized pioneering conferences. Attendees advocated logical formalism both as a means of structuring programming and of establishing its credibility through proof. Another boost came from the U.S. National Security Administration, which grew concerned about potential security breaches in new time-sharing installations. Advocates of artificial intelligence, who looked to build computers capable of logical reasoning, formed another vital strand in the discussion. Still others used computers to derive novel proofs of famed unsolved mathematical theorems, such as the one asserting that any map could be colored using just four colors.

None of this went forward without controversy. Some advocates of formal program proof resisted mechanization, literally clinging to fountain pens as the preferred tool of the trade. Many mathematicians joined them. More importantly, mathematicians and some voices in computer science challenged the whole idea that proof involved merely rigorous deductive logic of a sort machines could perform. In actuality, mathematical proof involved intuition and structured argument among a community of practitioners. It was essentially a social activity. Computer proof and program verification actually had more in common with logic than with mathematics. Advocates of program verification suffered further blows when attempts to use the technique in actual practice fell short.

As MacKenzie wades ever deeper into these intellectual disputes, readers without a strong commitment to comprehending the nature of proof or [End Page 894] a solid grounding in logic and computer science may well heed his advice that they "may wish to skip particular passages or even particular chapters while still following the overall narrative" (p. 13). Some of the material presented here taxes even MacKenzie's well-established ability to explicate sophisticated engineering science and make it comprehensible to nonspecialists. Part of the difficulty may be that he sometimes crosses beyond explication or even analysis and sounds instead like an active participant in the intellectual arguments under discussion. Based on close reading of the technical literature and interviews with key participants, his book in many respects reads like the latest contribution to the intellectual debates it chronicles.

This aspect of Mechanizing Proof comes into clearest view in its compelling concluding chapter. Here MacKenzie concedes that program proof and formal verification have exerted little direct influence on the actual practice of computing. Availability of cheap hardware, especially computer memory, relieved many of the underlying conditions that had raised concerns in the 1960s. Trust in computing in fact came to rely more...

pdf

Share