Required reading for anyone aspiring to develop or teach of computer systems.
Mechanizing Proof: Computing, Risk, and Trust
Donald A. MacKenzie
MIT Press Cambridge Massachusetts and London England 2001
This is an extraordinary book, for several reasons. It is a remarkably interesting and detailed snapshot of the history of the past half-century's efforts to formalize the foundations of the computer field and at the same time provide some serious rigor into the development of systems with critical requirements for dependability. The book is rather broad in its conception -- spanning (among other topics) computer science, programming and software development, hardware, mathematics, artificial intelligence, philosophy, dependability, trustworthiness, risks, and, above all, many people involved in seminal research and development. MacKenzie takes an objective view of his subject matter, considering the pros and the cons, the potentials and the pitfalls, the progress and polemics. Perhaps most noteworthy is that this book is written by a professor of sociology who has perspicuously captured the theory and practice with great depth of understanding. As a consequence, it will be an extremely valuable learning experience for computer professionals, and yet easily readable and very informative for nontechnical people interested in the history of supposedly dependable computers. This is a truly unusual combination!
Each chapter is interesting all by itself. The chapter on the proof of the four-color theorem is likely to be particularly fascinating to anyone curious about the worthiness of computer-based proofs. The chapters on applying rigorous analysis methods to computers are very informative. (Software was the original target of such methods, but hardware analysis is increasingly becoming not only cost-effective, but essential.) In summary, the last paragraph of the book is especially relevant:
"The proving machine, whether in the form of the automated theorem prover, the model checker, some hybrid of the two, or some other variant, is destined to become a permanent part of our technological and perhaps also our mathematical culture. Present and future generations will need to make decisions about the proper status and role of such machines. Treated as social prostheses, they are benign; treated as oracles, they become dangerous. If this book on the interactions among machines, proofs, and cultures helps this choice to be made wisely, it will have served a purpose."
This book succeeds wonderfully in characterizing the bases for such choices. Everyone aspiring to the serious teaching or development of computer systems needs to read it thoroughly early in their careers, and then to read it again later on after they have begun to more fully appreciate the risks of not doing things correctly. Ultimately, the dependability of computer systems relies on the knowledge, wisdom, and integrity of the individuals responsible for developing (as well as operating and using) those systems. That is perhaps the most important message of this book, which deserves the widest possible appreciation and understanding -- because it necessarily underlies the future of our increasingly technologically based civilization.
Peter G. Neumann, Principal Scientist, Computer Science Lab, SRI International, moderator of the ACM Risks Forum (www.risks.org), cofounder of People For Internet Responsibility (www.pfir.org), cochairman of the first two VERkshops on verification, whose proceedings appeared in the ACM Software Engineering Notes, July 1980 and July 1981.