I had planned to write a post later this spring on the collisions between what engineers sometimes perceive as practical and what turns out in practice to be useful. It’s a complex issue and there are examples that cut both ways, suggesting that a deeper understanding of both the underlying technology and the social “soup” where innovators thrive are needed to avoid some famous traps. I mentioned this briefly in my discussions of the impact of social fragmentation on innovation and the pitfalls of ignoring social contexts.
Then the January 2010 issue of Communications of the ACM crossed my desk. As I skimmed the contents, I was surprised to see my name in the headline of the Editor’s Letter, an attack by the Editor-in-Chief Moshe Vardi on a thirty-year-old paper [ Social Processes ] that I wrote with computing legend Alan J. Perlis and my colleague Richard J. Lipton (author of the popular Godel’s Lost Letter blog and subject of Dancing with the Stars ). The paper itself was controversial in its day and addresses exactly the WWC questions that I plan to write about. It is extraordinary for an Editor of a professional journal to use his position to make derogatory comments about articles, especially to further his own views. Mr.Vardi’s letter demanded a response. Lipton and I will jointly publish a longer and more technical essay on this subject at some point in the future, but today we are jointly publishing the following Letter to the Editor. The letter will also be sent to the Communications of the ACM.
In his Editor’s Letter in the January 2010 issue of CACM entitled “More Debate Please”, Moshe Vardi makes a plea for controversial topics in these pages, citing a desire to “let truth emerge from vigorous debate.” It is a sentiment that we support as well. But we question Mr. Vardi’s judgment in using his editorial position to mount an attack on colleagues who were neither forewarned nor given an opportunity to respond. Mr. Vardi’s target was our 1979 critique of formal program verification entitled “Social Processes and Proofs of Theorems and Programs,” It was co-authored with the late Alan Perlis, one of the originators of the field and a lifelong advocate for the kind of open discussion that the Editor advocates. We can only hope that future contributors have higher standards for debate than does the current Editor, because his out-of-context references to the 1979 debate over the practical efficacy of formal verification, his ex-cathedra determination that the article was “misguided” and his ill-informed view of the decision to publish it have no power to illuminate a serious subject.
We do not care to respond to Mr. Vardi’s substantial mischaracterizations and misstatements at this time, but we do think it is fair to point out that the publication of “Social Processes and Proofs of Theorems and Programs,” was not a singular event that might be classified as either misguided or not. “Social Processes” was a refereed article. A preliminary version was accepted by a highly selective conference program committee in 1976 and its presentation was attended by virtually every living contributor to the field. It was then submitted to this journal and reviewed by anonymous referees. Its publication was followed by many months of public presentations and workshops, letters to the Editor, written reinforcements and rebuttals, and — several years later — a special issue of this journal devoted to the topic. Mr. Vardi faults the editorial board for not publishing an opposing “counterpoint” article, a suggestion that — although it has all the “fair and balanced” trappings — would have been hard to reconcile with the confidentiality usually accorded to contributed articles that are sent to referees for review. The irony is not be lost on us that we were offered no such opportunity prior to publication of his letter.
The article itself has been reprinted dozens of times and has appeared in several anthologies in the philosophy of mathematics. Its publication and the ensuing debate have been the subject of social science research (Donald MacKenzie’s 2001 book “Mechanizing Proof” remains the definitive sociological and historical analysis of both the paper and its implications for the field). If our arguments seem off the mark to Mr. Vardi, then perhaps the right course of action is to resurrect the social process that led to the article’s publication in the first place and jump into the fray. Until that time, the correct editorial position for CACM and its Editor is to let both the paper and the written record that surrounds it speak for themselves. It strikes us as inappropriate, after thirty years of silence, to use the cover of an Editorship to attack unsuspecting passersby, especially while touting the moral virtues of free and vigorous debate.
 Donald MacKenzie, Mechanizing Proof: Computing, Risk, and Trust, MIT Press 2001, The Massachusetts Institute of Technology, Cambridge, MA