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.