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
Give Scratch an Abstraction Mechanism
I welcome the efforts described by Mitchel Resnick et al. in "Scratch: Programming for All" (Nov. 2009) to familiarize more people with programming. However, when I downloaded Scratch from the Scratch Web site (http://scratch.mit.edu) and looked over the Scratch programming constructions, I found no convenient abstraction mechanism, as in, say, a facility to define and call parameterized functions.
Such a mechanism could be viewed as advanced and not easily digested by the intended users of the Scratch programming language. But some projects on the Scratch Web site feature significant code redundancy and could be reduced in size and simplified if the code could be restructured through a few suitable functions.
Though not all Scratch programmers would be comfortable with an abstraction mechanism, it seems a pity that something so fundamental does not even exist, and so cannot be conveniently demonstrated and disseminated.
Second in importance and also missing from the Scratch programming language is a data-structuring mechanism.
Thorkil Naur and Karen Brahes, Odense, Denmark
Authors’ Response:
Abstraction is an important computational concept, and a simple form of procedural abstraction is provided by Scratch’s "broadcast" mechanism. That’s why we added parameterized procedures to some experimental versions of Scratch, though we have not yet come up with a design that satisfies our goals of simplicity and understandability. We’re continuing to experiment, hoping to include more forms of abstraction in future versions.
The Scratch Team, Cambridge, MA
Recognition for the Unaffiliated, Too
I was heartened by Wendy Hall’s interest, as expressed in her President’s Letter "ACM Europe" (Oct. 2009), in student chapters, award nominations, and conferences sponsored by the ACM in Europe.
I regularly seek out opportunities for public recognition and awards for ACM members not affiliated with universities. For example, the traditional rule requiring three or more endorsements for a researcher to be considered for an award is a barrier to would-be nominees not affiliated with universities or in the pool of preferred students of their academic mentors. The situation is even more problematic if an individual’s research is based on his/her long-standing experience in an area of expertise not currently "popular" in universities.
I therefore suggest the ACM in Europe establish a committee to consider self-nominations and invite volunteers from among the young researchers who promote computer science in their spare time, rather than as salaried academics.
Concerning conferences and other events, I’d also like to propose ACM set up summer schools open to all enthusiasts who promote electrical engineering and computer science. Locating them in popular tourist areas would be another way for ACM in Europe to increase interest in more traditional ACM activities and individual memberships.
Miroslav Skoric, Novi Sad, Serbia
Join the Discussion (0)
Become a Member or Sign In to Post a Comment