In the May 1979 issue of Communications, a powerfully written article by Richard A. De Millo, Richard J. Lipton, and Alan J. Perlis entitled "Social Processes and Proofs of Theorems and Programs," argued that formal verification of programs is "difficult to justify and manage." The article created the perception, in the minds of many computer scientists, that formal verification is a futile area of computing research.
That article did not cite a 1977 paper by Amir Pnueli entitled "The Temporal Logic of Programs." His paper had attracted little attention by 1979, but by 1997 it would be described as a "landmark paper" in the citation that accompanied Pnueli's 1996 ACM A.M. Turing Award. In his paper, Pnueli, whose sudden and unexpected death on Nov. 2, 2009 shocked the computer science community, laid the foundation for formal verification of concurrent and reactive programs. (An article describing Pnueli's scientific legacy appears on page 22.) The paper also laid the foundation for the development of model checking, an automated formal-verification technique for which Edmund A. Clarke, E. Allen Emerson, and Joseph Sifakis received the 2007 ACM Turing Award.
With hindsight of 30 years, it seems that De Millo, 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. Should we infer that Communications erred in publishing that article? My answer is a resounding "no!"
My basic education included exposure to Talmudic scholarship. Jewish scholars in the first half of the first millennium believed that truth will emerge from vigorous debate. The Talmud, a monumental work of Jewish scholarship concluded circa 500 CE, is in essence a compendium of legal debates. Vigorous debate, I believe, exposes all sides of an issuetheir strengths and weaknesses. It helps us to reach more knowledgable conclusions. To quote Benjamin Franklin: "When Truth and Error have fair Play, the former is always an overmatch for the latter." In my opinion, however, 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. Indeed, the article instigated so many reader responses, the editors published 10 pages of letters in the November 1979 Forum section of Communications, calling the work everything from "marvelous" to "humorous."
In 2007, when I met with various focus groups to discuss the relaunching of Communications, I was encouraged to keep this publication engaged in controversial topics. "Let blood spill over the pages of Communications," said one discussant jokingly. At the same time, however, participants believed that the magazine should represent all points of view fairly. This sentiment led to the establishment of the Point-Counterpoint feature, in which both sides of an issue are represented by opposing articles. Quoting Franklin again: "when Men differ in Opinion, both Sides ought equally to have the Advantage of being heard by the Publick."
Since the relaunch in July 2008, we have published several Point-Counterpoint pairs: on computing curricula, e-voting, Net neutrality, and the direction of CS education in the U.S. At this point, however, the pipeline for such articles is dry. I had assumed that both members of the editorial board and readers would propose topics for Point-Counterpoint articles, but that does not seem to be the case. It is almost as if people believe there is something improper about engaging in direct debate. In fact, several authors whom I invited to participate in Point-Counterpoint debates have declined in order to avoid head-on confrontation. The truth is, however, that there are many issues in computing that inspire differing opinions. We would be better off highlighting the differences rather than pretending they do not exist.
In this issue of Communications we have a debate that is quite a rarity in computing research: a technical debate. MapReduce (MR) is a software framework to support distributed computing on large data sets on computer clusters. It was introduced by J. Dean and S. Ghemawat of Google in a highly influential 2004 article, and featured as a Research Highlight paper in the January 2008 issue of Communications. The success of MapReduce led some to claim that the extreme scalability of MR will "relegate relational database management systems (RDBMS) to the status of legacy technology." A pair of Contributed Articles in this issueDean and Ghemwat on one side and Stonebraker et al. on the otherdebate the relative merits of MR and RDBMS beginning on page 64. As parallel computation is one of the hottest topics in computing today, I have no doubt that our readers will find this technical debate highly instructive.
If you have topics that you think should be debated on the pages of Communications, please contact me. More debate, please!
Moshe Y. Vardi,
©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.
The Digital Library is published by the Association for Computing Machinery. Copyright © 2010 ACM, Inc.
The following letter was published in the Letters to the Editor in the March 2010 CACM (http://cacm.acm.org/magazines/2010/3/76302).
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
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
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.
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.
Displaying all 3 comments