Retrospective: An Axiomatic Basis for Computer Programming

C.A.R. Hoare is one of those people who laid the very foundations of software engineering. He is probably best-known for inventing the quicksort algorith. He's also the one who invented the null pointer; the concept of a synchronization monitor in operating systems; and much more.

Forty years ago, Hoare published "An Axiomatic Basis for Computer Programming", aiming to formalize programming, under the belief that "an elegant formalization [of the semantics of a programming language] might consist of a collection of axioms, similar to those introduced by Euclid to formalize the science of land measurement." His hope was "to find axioms that would be strong enough to enable programmers to discharge their responsibility to write correct and efficient programs".

The quotes are from a new retrospective article, titled simply "Retrospective: An Axiomatic Basis for Computer Programming" and published in the October 2009 issue of Communications of the ACM -- the same journal that published the original paper. In this new paper, Hoare surveys changes in the field of software engineering over four decades, and compares them to his expectations and vision. In particular, he believed that software verification and proof will take off after "some accident or series of accidents involving loss of life, perhaps followed by an expensive suit for damages". But instead, any accidents -- such as the Ariane V crash in 1996 -- led to more rigorous testing, rather than a take-off of verification. Verification of software and axiomatic programming remained mostly an academic practice.

Surprisingly (for Hoare), what caused verification to be introduced into software development practices, to the extent that it is used, is security considerations: "the attack of the hacker, leading to an occasional shutdown of worldwide commercial activity". He claims that "the only way to reach these vulnerabilities is by automatic analysis of the text of the program", i.e., verification techniques. And what about testing? Testing is important, says Hoare, but not for testing the program; rather, they are used for testing the programmer.