Communications of the ACM
Forum
Forum
Thanks for Robert Glass's delightfully written history ("The Proof of Correctness Wars," "Practical Programmer," Aug. 2002). As a mathematician and a computer scientist, I have always been saddened that proof-of-correctness methodology never worked out, but as a practical programmer I understand why.
I remember discussing the proof-of-correctness effort to verify the correctness of the INMOS Transputer chip's floating point processor with one of the participants, a computer scientist from Oxford. (This was part of the British Ministry of Defence-mandated effort to formally verify real-time hardware and software Glass alludes to in his column.) The verification effort took three or four times longer than the actual design, though it did uncover several subtle flaws.
The problem with proof-of-correctness efforts has always been the extremely primitive deductive systems people are forced to use. In mathematics, almost all theorems are proved using an informal but rigorous language of discourse based on ordinary English (or Russian, or French, or ...) coupled with what the late logician Abraham Robinson called "the language of functions and relations." Despite the beauty of well-designed programs and the enormous kick of seeing them work, mathematics, by contrast, seems to soar (after the months of often frustrating effort to rough out a proof in the first place). But when mathematicians use a completely formal, low-level deductive system, it can take hundreds of pages to prove even the simplest things. For example, it takes several hundred pages for Russell and Whitehead to prove that 1 + 1 = 2 in Principia Mathematica.
We computer scientists are well aware of this issue of language level, appreciating how difficult it is to write programs in assembly language. I believe proof-of-correctness efforts have failed because they force people to write the proofs in the assembly language of mathematics. What we desperately need is a suitable higher-level language in which to express proofs of correctness, coupled with compiler-like software to mechanically translate the higher-level, necessarily incomplete proof into a complete and correct lower-level proof that could then be mechanically checked.
The OO programming community has already taken us part of the way there. UML and the widely available UML modeling tools provide a start on the higher-level language and the compiler-like software for formal checking. But much more needs to be done.
A fundamental logical obstacle complicates this effort. Filling in incomplete informal proofs brings us up against the "undecidability" theorems of modern logic, especially Turing's theorem on the undecidability of the halting problem. What just might make a proof-of-correctness compiler possible is, first, that good programmers write good code they basically understand to be correct, and, second, the interactive nature of modern computation. As to the first point, any proof-of-correctness compiler will exceed its time limits and fail to verify or refute some arbitrary proofs, but the informal proofs produced by good programmers would (one hopes) almost always be structured well enough for complete analysis and translation.
As to the second point, a proof-of-correctness compiler could be written so it halts when it gets stuck and asks the human programmer for guidance. As good programmers usually know why their programs (almost) work, the human programmer would probably be able to give the compiler enough proof hints so it can finish its job.
The current emphasis on security in software illustrates why a workable proof-of-correctness technology is needed now more than ever. It has to be semiautomated to be workable. I suggest that creating and perfecting a workable proof-of-correctness technology ought to be included among the Grand Challenge Problems of computer science.
C.W. Neville
West Hartford, CT
DeMillo, Lipton, and Perlis (Communications, May 1979) provided important reasons why social processing of correctness proofs in computer science is highly unlikely to provide the degree of assurance often attained for deductive proofs in logic and mathematics. As a result, the acceptance of programs as correct by the members of the computer science community does not represent as stringent a condition as does acceptance of proofs of theorems in the logic and mathematics community.
However, while formal proofs are sometimes able to prove what abstract machines do when they execute programs, they cannot possibly prove what will actually occur when physical machines execute programswhich remains true even when those programs happen to be correct. Not only are correctness proofs subject to practical limitations, as DeMillo, Lipton, and Perlis explained, but even if program proofs were as good as gold, they cannot guarantee what will happen when they are executed by systems that control cruise missiles, land aircraft, or perform radiation therapy.
The kind of knowledge formal proofs alone can supply simply does not extend to the performance of causal systems. To believe otherwise is to commit a category mistake. In an otherwise excellent discussion of "the program verification debate," Jon Barwise (Computers and Mathematics, Sept. 1989) suggested that I commit (what he calls) "the fallacy of identification" by confounding programs-as-text with programs-as- executable-code. But this is the kind of mistake that underlies efforts to model computer science on pure mathematics, when it is an applied mathematical discipline. Computers are physical systems embedded in the world.
The language of models applies, where models stand for the things they model. Programs are models1 of solutions to problems, typically in the real world. Languages in which they happen to be written are models2 of machines, which may exist only in the abstract. Sometimes those machines are linked to physical machines by compilers or interpreters, that translate them. Machine language itself, is, in turn, a model3 of the target machine. Formal proofs can no more guarantee these models are true of systems embedded within the world than verifying its blueprints can guarantee a house is properly built. The same applies to formal proofs of hardware.
It is not even a theoretical possibility. Alternatively, view programs as conjectures. The question is not whether they conform to the beliefs of those who construct them, but whether they are true as claims about the world. Not only must they be true as conjectures about their solutions to problems, high-level and low-level languages, and causal influence on target machines, but those target machines themselves must be embedded within the physical world through their causal connections to the totality of apparatus with which they must interact for them to hit targets, land planes, or irradiate tumors.
Formal methods can contribute to securing program correctness, especially when those programs are modest enough to welcome social processing. But only empirical procedures, including program testing and debugging and prototype construction and testing, are even the right kind of methods for predicting the future performance of a causal system in the world. Even then, the state of the system in the future may differ from the state of the system in the past, yielding misleading results. Such knowledge is tentative and fallible, which is why attempted executions of programs so often turn out as refutations.
Classic studies of the scope and limits of formal methods in computer science are collected together by T. Colburn, et al. in Program Verification: Fundamental Issues in Computer Science (1993). In addition to those cited here, my own more recent contributions include Minds and Machines, May 1991, and Bridges 5, 1998. Personally, I would be astonished if any members of the community continue to insist the performance of a machinean actual physical machine, not an abstract counterpartwhen executing a program can be guaranteed by formal proofs. In that sense, I presume, the program-verification debate has been resolved.
James H. Fetzer
Duluth, MN
How well I remember the proof-of-correctness wars. My position was (and still is) intermediate and unrepresented, but other than to a couple of trusted associates, I did not dare discuss it much, knowing that in a highly polarized climate, moderates usually get caught in a crossfire between both extremes. But Glass's column has prompted me out of the closet.
One of the arguments against program proofs was that the examples were all toy problems, and for real-size programs implemented by software practitioners, proofs would be so lengthy as to be utterly intractable. All the more so today, as we write substantially larger programs. But we teach programming in part by teaching tracing, often explicitly, on paper, again only for beginning-student-size examples. Tracing a real-size program is just as intractable as proving it, yet I believe many programmers, in writing large programs, nevertheless use mental processes based on tracing.
It ought to be possible to do learning exercises in constructing program proofs explicitly, letting it become the basis of a thinking style that can be carried into practitioner-size programming tasks in the same way. I recall that during the wars, I heard it said that a number of proofs of small code fragments (that today might be called idioms) would constitute a body of theorems about these idioms. The idioms could then be reused repeatedly, appealing to the theorems without reproving them.
The advantages are obvious in that a trace tells something about only an individual computation, while a proof tells something about the whole algorithm. All programmers can improve their skills by thinking algorithmically instead of computationally, and doing so inevitably results in fewer bugs in released software. Reading and writing proofs for small algorithms seems like an excellent learning method for doing so.
Having said that, I wish to emphasize that students need to be taught computational thinking first. To do otherwise would be like trying to teach algebra without first teaching arithmetic. You can't think effectively about whole classes of computations until you understand individual computations.
Rodney M. Bates
Wichita, KS
I read Glass's column with much interest. I have no idea whether there will be another such war, but if there is, I believe it will be much more productive than the last two, because a large body of software is free to download. Program-verification advocates have the opportunity to clearly demonstrate the benefits of their methodologies on this software, which includes several surprisingly full-functioned operating systems, a number of compilers, a symbolic mathematics program, and much more.
Some are rising to this "put up or shut up" challenge. One modest but useful example is the Stanford Checker, which has found a number of problems in the Linux kernel. Similar tools, including the Unix "lint" command and any number of integrated development environments. Of course, such tools are but an impoverished shadow of the late-1970s verification advocates' grand vision. On the other hand, a visionary whose vision could be fully realized in two decades would certainly be an extremely poor excuse for a visionary.
Paul E. McKenney
Beaverton, OR
We found Glass's column insightful and timely in capturing the essence of the history of the debate surrounding the use of formal methods. Since Glass laments the "almost total absence of evaluative research findings on the matter," we would like to point to the existence of a recent such finding on teaching and using formal methods in an academic setting (see the March 2002 issue of the IEEE Transactions on Software Engineering). There, we describe one result from a three-year-long, controlled, educational experiment in which two sets of undergraduate software engineering students were taught identical material, except one group was also taught formal analysis. Although we have no wish to start another ugly battle in the war Glass describes, we hope this result inspires further evaluative research.
Ann Sobel
Miami University
Michael Clarkson
Cornell University
Handling Web Content
Hal Berghel would lay the woes of the creative world at the feet of Google, America Online, and the other proprietors of Web caches and simultaneously blame them for wholesale violations of copyright law, demanding they provide a warm and fuzzy infrastructure for the creators to provide irrelevant details about their content to the Web caches. The real solution is much simpler but requires the creators take responsibility for learning to use the existing methods to exercise the control they desire over their own intellectual property.
Berghel poses several questions regarding the handling of content on the Web, many of which have already been considered and can be easily resolved using existing methods. For example, a lack of usage statistics on cached content can be easily fixed by adding a dynamically generated object to the Web page that cannot be cached. This does not have to involve privacy issues any more than current logging practices do. However, Berghel chooses to sensationalize the issue by mentioning only the charged phrase "Web bugs" as a solution. This serves only to raise the emotions of his readers, rather than taking an objective view of the problem at hand and the solutions available.
He also tries to claim it is not realistic to expect content creators or publishers to learn about and use existing cache controls to protect their intellectual property. But his solution is to add more cache control directives for content creators to use. Adding complexity does not solve the problem of controlling intellectual property on the Web. It only makes it more difficult for creators and publishers to understand how their content will be handled. One of the largest cache operators on the Internet, America Online, already provides a tutorial Web site at webmaster. info.aol.com to inform publishers of how to work with the cache rather than just complain about it.
As with many political issues surrounding intellectual property and the Internet, what is required is education and use of the existing methods, not additional standards and legislation. Cache operators should not be forced to worry about copies of a piece of content that may have been published on more than one Web site. Nor should they be responsible for collecting or managing royalties. If cache operators are forced to handle royalties, or support a myriad of cache control directives that either cause a significant degradation in the usefulness of the cache or an increase in the amount of support cache operators must provide, Web caches will cease to exist. And while many publishers look forward to that day, they would quickly find that the drastic increase in traffic to their Web sites would cause their costs to increase proportionally.
Responsibility for publishing content in a way that achieves copyright controls belongs to the content creators and publishers; they must assure their content is not published in multiple locations unless desired. They must assure that proper authentication controls are used if they wish to limit access to their work. And they must track down and address violations of their copyright using the existing intellectual property laws. Distribution control of content is in the hands of the content creators, if only they would take an active role in exerting that control.
Todd Palino
Sterling, VA
Hal Bergel Responds:
There's less to Palino's response than meets the eye. Article 9 of the Berne Convention for the Protection of Literary and Artistic Works (www.wipo.org/ treaties/ip/berne/) ratified by the U.S. March 1, 1989 states:
"Authors of literary and artistic works protected by this Convention shall have the exclusive right of authorizing the reproduction of these works, in any manner or form."
Some of us believe in the Berne Convention. Apparently, Palino does not. The battle line may be drawn that simply.
Note the wording "in any manner or form." This mandate does not contain the caveat "unless some ISPs or portals find it inconvenient to conform to this treaty." Nor does the Berne Convention imply that intellectual property rights are bipolar. In the real world, authors have more options than the extremes of refusing anyone access to their work on the one hand, versus giving up all rights to their intellectual property on the other. I proposed in my column that the cache-control directives be brought into conformance with the international laws governing intellectual property in modern societies.
Does that mean cache serving is inherently bad? Of course not. As I stated in my column, caching serves a useful role in making networks more efficient. The problem is that current caching strategies are designed for the convenience of those who maintain cache servers and are insensitive to intellectual property rights that all democratic governments worthy of the name recognize as fundamental. Members of the World Wide Web Consortium and the Internet Engineering Task Force, well-intentioned and dedicated as they are, are not immune to occasional myopia. Cache control is a case in point, cookies are another.
Palino claims that all the cache controls the world might need are already available. I leave it to the readers to see how one may prevent caching from for-profit portals while allowing it for not-for-profit portals. Or try to define the semantic constraints of the document tokens to be cached within the existing framework. Simply stated, you can't get there from here.
Palino also asserts that the "content creators and publishers ... must track down and address violations of their copyright using the existing intellectual property laws." Authors, artists, and musicians beware: on this view, copyright law is a core element of your creative enterprise.
©2002 ACM 0002-0782/02/1200 $5.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 © 2002 ACM, Inc.
No entries found