Letter to the Editor

In the May, 1979 CACM, De Millo, Lipton, and Perlis published an influential paper titled Social Process and Proofs of Theorems and Programs. This paper made some excellent observations. However, by throwing in a few red herrings, they came to some wrong conclusions about program verification. More insidiously, they framed the debate as one between a reasonable engineering approach that completely ignores verification and a completely unrealistic view of verification advocated only by its most naive proponents. (There were, unfortunately, quite a few such proponents.) At that time, some ACM publications had a special section on algorithms. In an ironic coincidence, the same issue of CACM carried the official ACM policy on algorithm submissions. It included all sorts of requirements on the form of the code, and even on the comments. Missing was any requirement that the correctness of the algorithm be demonstrated in any way. I was appalled at the idea that, ten years after Floyd and Hoare’s work on verification, the ACM was willing to publish algorithms with no correctness argument. The purpose of my letter was to express my dismay. I ironically suggested that they had succumbed to the arguments of De Millo, Lipton, and Perlis in their policy. As a result, my letter was published as a rebuttal to the De Millo, Lipton, and Perlis paper. No one seems to have taken it for what it was–a plea to alter the ACM algorithms policy to require that there be some argument to indicate that an algorithm worked.