Letter to the Editor
Communications of the ACM 22 | , Vol 11: pp. 624
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.
Copyright © 1979 by the Association for Computing Machinery, Inc.Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, to republish, to post on servers, or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from Publications Dept, ACM Inc., fax +1 (212) 869-0481, or email@example.com. The definitive version of this paper can be found at ACM's Digital Library --http://www.acm.org/dl/.