Communications of the ACM

Footnotes

DOI: http://doi.acm.org/10.1145/1629175.1629176

©2010 ACM  0001-0782/10/0100  $10.00

Permission to make digital or hard copies of all or part 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. To copy otherwise, to republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee.

CACM Administrator

The following letter was published in the Letters to the Editor in the March 2010 CACM (http://cacm.acm.org/magazines/2010/3/76302).
--CACM Administrator

In his Editor's Letter "More Debate, Please!" (Jan. 2010), Moshe Y. Vardi made a plea for controversial topics on these pages, citing a desire to "let truth emerge from vigorous debate." Though we support the sentiment as well, we question Vardi's judgment in using his editorial position to mount an attack on a 30-year-old article whose authors were neither forewarned nor given the opportunity to respond. Vardi's target was our 1979 critique of formal program verification, "Social Processes and Proofs of Theorems and Programs," co-authored with the late Alan J. Perlis, winner of the first ACM A.M. Turing Award and lifelong proponent for the kind of open discussion Vardi himself advocates.

It is an extraordinary event when the Editor-in-Chief of a professional journal uses his position to declare ex cathedra that a published article is "misguided," its arguments "off the mark," and prior editors "did err in publishing [the] article... without publishing a counterpoint article..." The irony is not lost on us that we were offered no such opportunity to respond prior to publication of Vardi's Letter.

We completely disagree with Vardi's assessment and will respond to the technical substance of his comments at a later time. However, we stand by the article's two major predictions:

* That human-written proofs of real systems would not work due to the lack of the "social processes" that drive confidence in mathematical proofs. Even today, there are no human proofs of real systems; and
* That formally specifying real systems would continue to be impossibly difficult, a position since vindicated by history. Where are the formal specifications for Windows 7, thousands of iPhone apps downloaded daily, and hundreds of thousands of other systems used every day in research, commerce, and government? They do not exist.

Publication of "Social Processes and Proofs of Theorems and Programs" was not a singular event. It was refereed. A preliminary version was accepted by a highly selective conference program committee in 1976 predating by more than a year the article by Amir Pnueli that Vardi criticized us for not citing and its presentation was attended by virtually every living contributor to the field. It was then submitted to Communications and reviewed by anonymous referees. Its publication was followed by months of public presentations and workshops, letters to the editor, written reinforcements and rebuttals, and years later a special issue of Communications devoted to the topic.

The article was widely read and commented on by computer scientists, engineers, and mathematicians but, rather than spark debate in the formal verification community, provoked only stony silence. A quick scan of the formal verification literature in the years 19791990 reveals virtually no citations to the article. In what sense is an article "controversial" if one side refuses to engage in discussion? Indeed, email circulating among the principals in the field aimed to tamp down debate and ignore our argument that many outside the field still consider substantial and prescient.

The field of formal program verification has changed substantially since 1979. Its goals have become more modest and its claims less sweeping. New methods have emerged. An equally compelling reading of history suggests that, during the long silence, the formal verification research community realized it had been misguided in 1979 and used the arguments without attribution set forth in the article as a roadmap to reorient its agenda.

The article itself has been reprinted dozens of times, as well as in several anthologies in the philosophy of mathematics. Donald MacKenzie's book Mechanizing Proof: Computing, Risk, and Trust (MIT Press, Cambridge, MA, 2001) remains the definitive sociological and historical analysis of both the article and its implications for the field. If, to Vardi, our arguments seem off the mark, then perhaps the right course 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 Communications and its Editor-in-Chief is to let both the article (and the written record that surrounds it) speak for itself.

It is inappropriate, after 30 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.

Richard A. DeMillo and Richard J. Lipton
Atlanta, GA

-----------------------------------------

AUTHOR'S RESPONSE

It seems both DeMillo and Lipton feel slighted by my Editor's Letter (Jan. 2010). I had no intention of slighting them or the article in question and apologize for unintentionally causing them to feel this way.

Now to the substantive points in their comment:

1. I am accused of using my editorial position to "mount an attack" on an article published in Communications in 1979. DeMillo and Lipton imply that it is inappropriate for an Editor-in-Chief to comment negatively on an article published in Communications.

The article in question is more than 30 years old. History, it is said, "judges and rejudges." I hardly view my offering of some comments, even if critical, on such a historically important article as "mounting an attack." Personally, if someone saw the need to disagree with an article of mine 30 years after its publication, I'd feel complimented. Most articles are long forgotten after 30 years.

Regarding whether it is appropriate for an Editor-in-Chief to comment on articles published decades earlier, one should note that even the U.S. Supreme Court occasionally reverses itself. I never heard of "stare decisis," the principle that precedent decisions are to be followed by the courts, being applied to editorial matters across such a time span. (In contrast, when I assumed the position of Editor-in-Chief, I committed to respecting all prior editorial decisions in regard to pending submissions to Communications.)

2. I am accused of not offering DeMillo and Lipton an opportunity to respond prior to publication of my Editor's Letter. As Editor-in-Chief I write such bimonthly Editor's Letters in which I often express opinions on controversial matters. The proper way to disagree with them, and many people do, is to leave comments online or submit a letter to the editor. This is standard operating procedure in all publications I am aware of.

As Editor-in-Chief, I am committed to a scrupulous peer-review process for submitted articles, but I have not taken a vow of silence, nor does it make sense for me to do so. Furthermore, I gladly welcome the Editor-in-Chief in 2040 to reexamine my editorial decisions.

3. It seems that DeMillo and Lipton were offended by my use of the word "misguided." But one should read the full context of the word: "With hindsight of 30 years, it seems that DeMillo, Lipton, and Perlis' article has proven to be rather misguided. In fact, it is interesting to read it now and see how arguments that seemed so compelling in 1979 seem so off the mark today."

In the paragraph that preceded these sentences, I referred to two Turing Awards given for works in formal verification. Due to lack of space, I did not include references to two ACM Kanellakis Awards and two ACM Software System Awards for works in formal verification.

It is in this context that I expressed an opinion that the 1979 article, which implied the futility of formal verification as an activity and, by implication, as a research area was "misguided," with "hindsight of 30 years" in spite of "its compelling arguments."

4. DeMillo and Lipton disagree with my opinion that "the editors of Communications in 1979 did err in publishing an article that can fairly be described as tendentious without publishing a counterpoint article in the same issue."

The subject (and title) of my editorial was "More Debate, Please!" The article in question is one of the most controversial and influential ever published in Communications. I read it as a graduate student and was deeply affected by it. I singled it out because it was the perfect example for making the point of my editorial, which did not focus on analyzing the 1979 article. Rather, its main point was that, in my opinion, even with 30year hindsight, the editors in 1979 did absolutely the right thing in publishing it.

It is precisely because the 1979 article was so influential that I chose it as an example. I honestly feel that its authors should be pleased that it is still trenchant, even if some people disagree with its major thrust.

I am well aware of the process that led to its publication in 1979. I stand behind my opinion about the lack of a counterpoint article. DeMillo and Lipton are entitled to a different opinion. We may need to agree to disagree on this one. I do not see why this is an issue that deserves such a strongly worded response, when I expressed strong support for the editorial decision to publish the article, even with the hindsight of 30 years.

5. I'd rather not respond here to DeMillo and Lipton on the merits of their article. I would, however, welcome a new article from them examining the issues they covered in 1979. I would of course seek to publish a counterpoint article in the same issue.

Moshe Y. Vardi
Editor-in-Chief

Victor Yodaiken

Vardi's comment neglects the difference between "formal methods" as used in practice and "formal methods" as advocated by e.g. Dijkstra and Hoare at time Perlis et al wrote their paper. I very much doubt that Dijkstra would have considered the verification of the CompCert compiler as an example of the kind of mathematical reasoning about programs he had in mind. In fact, time has shown Perlis et al were correct. Programs to reason about and validate programs have become more sophisticated, but they have little to do with Hoare's axiomatic methods or similar.

Moshe Vardi

To the contrary. Formal methods today very much build on the ideas pioneered by Dijkstra and Hoare. Hoare's "An axiomatic basis for computer programming" has over 6,000 citations, and is still heavily cited today. Of course, formal-methods has made many advances over the past 40+ years, as is expected.