Chapter 2 of Professor Donald MacKenzie’s Mechanizing Proof (2001) asks why anyone wanted to prove computer programs correct in the first place.
One early use of computers was monitoring for attacks in real time, where a software error had direct consequences: in 1960, an early-warning radar system read echoes from the rising moon as a large incoming attack. Meanwhile, large software projects of the 1960s were routinely late, over budget, and full of bugs. This was the “software crisis” that led a 1968 conference to coin the term “software engineering.” Professor Fred Brooks compared large-system programming to a tar pit, where projects get stuck however capable the team.
The chapter then surveys the proposed boardwalks across it. One was disciplined method, such as Professor Edsger Dijkstra’s structured programming. The other, the subject of the book, was mathematical proof of program correctness, developed by Professors McCarthy, Naur, Floyd, and Hoare. Professor Dijkstra supplied the argument for it: testing can show that bugs exist, never that they are absent. Only proof promised certainty.
This motivation shapes the rest of the book. Hand proofs of real programs were too laborious and error-prone, so proof itself had to be automated, which leads to automated theorem provers (ch. 3) and their use in government security work (chs. 4–5). Mechanized proof also became a rival to proof as mathematicians practice it. Professor MacKenzie argues our culture now holds both ideals, and they clash in the DeMillo–Lipton–Perlis debate (ch. 6) and in the VIPER chip and prover-bug cases (chs. 7–8). His conclusion: mechanized proof does not remove the need for trust in human judgment. It relocates it to specifications, models, and the provers themselves.
The boardwalks still rest on something.