How clear is the proof?

Mechanizing Proof (Computing, Risk and Trust) by Donald MacKenzie

During the 1970s and 1980s automated verification of program correctness promised so much. You’d be able to take your program, mathematically specify what you expected the program to compute, and then let a theorem prover check that the program satisfied the requirements. Indeed, when I was doing my Phd in 1991, one of the potential projects was the verification of the specification of a washing machine controller.

Things turned out not to be so easy though. What did it mean to prove that a program was correct? How can you be sure that a positive result from a verification tool really means that the program is correct? How do you know that the specification is correct?

This book addresses these questions and at the same time gives the history of the automated verification from its early days until the turn of the century. The author has taken lots of material and converted it into an informative and provocative book which discusses what mathematical proof actually is, and whether this kind of proof is really what we want when we say that a program has been verified. he asks whether it is meaningful to verify at program without also verifying the hardware on which the program runs.

Fascinating, interesting and thought provoking.

This entry was posted in Books. Bookmark the permalink.

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s