Hoare on Testing

On the flight to the ISO C standards meeting this morning, I was reading this month’s issue of CACM, and found that Sir C.A.R. (Tony) Hoare wrote a nice piece called Retrospective: An Axiomatic Basis for Computer Programming.

Hoare has long been a noted proponent of axioms and formal proofs of program correctness. In that light, the following passage on testing and axioms struck me as well put and I thought I’d share it (emphasis added):

One thing I got spectacularly wrong. I could see that programs were getting larger, and I thought that testing would be an increasingly ineffective way of removing errors from them. I did not realize that the success of tests is that they test the programmer, not the program. Rigorous testing regimes rapidly persuade error-prone programmers (like me) to remove themselves from the profession. Failure in test immediately punishes any lapse in programming concentration, and (just as important) the failure count enables implementers to resist management pressure for premature delivery of unreliable code [or forces management to be explicitly unreasonable in the face of bug bar data and specific failure cases having an objective severity –hps]. The experience, judgment, and intuition of programmers who have survived the rigors of testing are what make programs of the present day useful, efficient, and (nearly) correct. Formal methods for achieving correctness must support the intuitive judgment of programmers, not replace it.

My basic mistake was to set up proof in opposition to testing, where in fact both of them are valuable and mutually supportive ways of accumulating evidence of the correctness and serviceability of programs. …

He also mentions many other useful observations and reminds, including the value of assertions to find, not run-time errors, but programming bugs. (See also C++ Coding Standards Item 68: Assert liberally to document internal assumptions and invariants.)

The whole article is good reading, and not long. Recommended.