Mechanizing Proof: Computing, Risk, and Trust (Inside Technology) [Paperback]

Donald Mackenzie (Author)

Book Description

Series: Inside Technology | Publication Date: January 30, 2004

Most aspects of our private and social lives -- our safety, the integrity of the financial system, the functioning of utilities and other services, and national security -- now depend on computing. But how can we know that this computing is trustworthy? In Mechanizing Proof, Donald MacKenzie addresses this key issue by investigating the interrelations of computing, risk, and mathematical proof over the last half century from the perspectives of history and sociology. His discussion draws on the technical literature of computer science and artificial intelligence and on extensive interviews with participants.MacKenzie argues that our culture now contains two ideals of proof: proof as traditionally conducted by human mathematicians, and formal, mechanized proof. He describes the systems constructed by those committed to the latter ideal and the many questions those systems raise about the nature of proof. He looks at the primary social influence on the development of automated proof -- the need to predict the behavior of the computer systems upon which human life and security depend -- and explores the involvement of powerful organizations such as the National Security Agency. He concludes that in mechanizing proof, and in pursuing dependable computer systems, we do not obviate the need for trust in our collective human judgment.

Editorial Reviews

Review

"A most readable account of how program verification came to promise so much and deliver so little." - Richard Clayton, The Times Higher Education Supplement"

About the Author

Donald MacKenzie is Professor of Sociology (Personal Chair) at the University of Edinburgh. His books include Inventing Accuracy (1990), Knowing Machines (1996), and Mechanizing Proof (2001), all published by the MIT Press. Portions of An Engine, not a Camera won the Viviana A. Zelizer Prize in economic sociology from the American Sociological Association.

Product Details

• Paperback: 440 pages
• Publisher: The MIT Press (January 30, 2004)
• Language: English
• ISBN-10: 0262632950
• ISBN-13: 978-0262632959
• Product Dimensions: 8.6 x 5.6 x 1 inches
• Shipping Weight: 1.4 pounds (View shipping rates and policies)
• Average Customer Review: 5.0 out of 5 stars  See all reviews (1 customer review)
• Amazon Best Sellers Rank: #1,412,078 in Books (See Top 100 in Books)

More About the Author

Discover books, learn about writers, read author blogs, and more.

Customer Reviews

Most Helpful Customer Reviews

4 of 4 people found the following review helpful:

5.0 out of 5 stars An excellent proof, October 7, 2006

By 

Dr. Lee D. Carlson (Baltimore, Maryland USA) - See all my reviews
(VINE VOICE)    (HALL OF FAME REVIEWER)    (REAL NAME)   

Amazon Verified Purchase

This review is from: Mechanizing Proof: Computing, Risk, and Trust (Inside Technology) (Paperback)

Professional mathematicians typically never argue about the methods of proof that they use, although they argue quite frequently whether a collection of statements does indeed constitute a proof. The development of a proof can take years in some cases, but the discovery of an error in a proof involves relatively short scales of time. The proofs that mathematicians subject to peer review are a mixture of natural language and mathematical symbolism, but the deductive nature of the steps in the proof are readily apparent, and the mathematical community has deemed this style of mathematical scholarship acceptable. This informal structuring of a mathematical proof is to be contrasted with that insisted upon by logicians, who insist that a proof should be a listing of formal statements, with each being a deduction from prior ones. If natural language appears it is only as metamathematical commentary and is set apart from the proof itself. These proofs are thus difficult for a human to read, unless they have in-depth knowledge and experience of the formalism that is used. This style of (formal) proof has been followed by those involved in research in automated theorem proving or in the very important field of formal verification. The discovery of a new proof of an old mathematical result or the discovery of new concepts in mathematics by a machine is the goal of this research, and it has had varying degrees of success in the last few decades.

If an error were discovered in one or more of the many mathematical results that exist in the literature, it would bring no risk to human society in general. These results are usually highly esoteric, and have no practical application, so any error discovered in them would probably only cause pain to the mathematician(s) responsible for them. However, computer scientists have realized that huge software programs that are critical to business, industry, and government are efficiently analyzed in the framework of certain mathematical structures. The flow of the program can be viewed as a deduction, in a manner very similar to what goes on in proofs of mathematical results. It is essential that these programs are without error (or "bugs"), and thus error-checking becomes proof-checking in this approach. This brings up of course the question as to whether these proof-checkers are themselves free of error. Who is to decide whether a sequence of statements, be they a software program or a series of formal deductions, do not contain errors?

This question, along with many other highly interesting topics, is discussed in this book. It could be read by anyone interested in automated theorem proving, formal verification, automated mathematical discovery, natural language processing, and artificial intelligence. The author has done an excellent job of articulating on the nature of proof, both formal and informal, and the risks involved in trusting machines to verify the reliability of both hardware and software. The latter is the main issue in the field of formal verification, and is one that is of immense importance in the modern world, whose technological complexity is increasing hyper-exponentially. It is because the machines and technology of today are so complex that one needs an effective methodology for checking their design and functioning to ensure that they are not flawed to a degree that may cause death or needless suffering to human beings. Can we trust a machine to check the design of medical equipment or do a verification of software? What if the machine makes a mistake or is itself the result of a faulty design? And for highly complex equipment or software, will the results of the machine check be comprehensible to a human?

The author outlines the history of proof theory, proof checking, and formal deduction, and includes anecdotal discussion of some of the researchers in these areas. For this reviewer, the most interesting part of the book was the last two chapters, for it is here that the author discusses the societal impact of machine proof. One learns for example that some of the early implementations of machine proof allowed a substantial amount of "hints" from the human user. This is not really surprising, since early developments in artificial intelligence can be characterized by the need for inputs from a human tutor. The goal of course is to free the machine from the need for this tutoring, and become essentially independent, to "think for itself". The author clearly believes that this presents a danger, and he points to the need for continued interactions between the machine and society in order that decision-making is carried out safely and in a way that is productive to human society as a whole. He believes that treating proving machines as "oracles" is dangerous, but he realizes that these kinds of machines have become a "permanent part" of our culture.

The author's anxiety is somewhat unjustified if one takes cognizance of the fact that the use of these kinds of machines is due to the efforts of human researchers, who have a thorough understanding of their functioning and limitations. And these machines are not autonomous. Their skill and efforts in proof checking, theorem proving, or formal verification is due solely to the instigation of a human investigator. But his anxiety is justified if judged relative to future developments. With each passing day, we place more of our trust in these types of machines, among many others, who are now responsible for financial decision-making, drug discovery, network management, legal casework, and myriads of other socially beneficial functions. It is becoming more rare to discover that these machines have made a mistake, but it is also becoming rarer for humans to take the initiative to find any mistakes. As machines are designed to become more autonomous they will themselves take the initiative to engage in activities that may or may not be deemed useful to human societies. The degree of symbiosis between the human and machine communities will therefore be directly proportional to their mutual trust.