steve@hubcap.clemson.edu ("Steve" Stevenson) (01/08/90)
I'm trying to discover the real reason why people do not prove their programs are correct. I would like to collect those reasons --- even those snappy one liners that we all use as excuses. Please forward your comments ( short flames ok) to me by E-mail. I'll post the replies if there is sufficient interest. Thanks. Steve (really "D. E.") Stevenson steve@hubcap.clemson.edu Department of Computer Science, (803)656-5880.mabell Clemson University, Clemson, SC 29634-1906 -- Steve (really "D. E.") Stevenson steve@hubcap.clemson.edu Department of Computer Science, (803)656-5880.mabell Clemson University, Clemson, SC 29634-1906
phil@umn-d-ub.D.UMN.EDU (Philosophy Dept) (02/25/90)
Charles Martin's intermperate tirades concerning my position are not even coherent. He belittles what he calls "Fetzer's Dilemma" as irrelevant and insignificant, while simultaneously attacking what he calls "Hoare's Folly" as relevant and significant. Since Fetzer's Dilemma itself was a critique of Hoare's Folly, Martin's position is not even consistent. Apparently, if he criticizes a position, then it is important, but not if someone else does. My arguments concern whether computer science should be viewed as a branch of pure mathematics or as a branch of applied mathematics. The dilemma that I posed arises from the realization that purely deductive reasoning cannot pro- vide content about preformance for any physical machine, so that if we want content about performance of a physical machine, then purely deductive reason- ing is not enough. I do not deny that correctness proofs can be pursued as a branch of applied mathematics, but their limitations--in principle and in prac- tice--must be clearly defined. As examples of Martin's selective distortion of the real issues at stake here, observe that, in his message of 20 January 1990 at 15:11:42, he maintains, "As a practical matter, the issues Fetzer raised in his diatribe passing false- ly as a technical article can be largely ignored, both from the standpoint of engineering and mathematically." Consider, however, what this person would have you ignore (some of the most important consequences of my position): "If one were to assume the execution of a program could be anticipated with the mathematical precision that is characteristic of demonstrative domains, then one might more readily succumb to the temptation to conclude that de- cisions can be made with complete confidence in the (possibly unpredictable) performance of a complex causal system" (CACM 31/9 (1988), p. 1062). Perhaps this is a matter he wants to ignore, but the rest of us do so at our peril. In his message of 25 January 1990 at 18:07:15, he states that, "Fetzer's argu- ment is precisely that program proofs are flawed on the face, that no proof can ever give insight or certainty to the behavior of a real program on a real machine, because of the distinction between the mathematical model and the real world." Since part of what he says here is correct (the last part), it gives a specious plausibility to the rest (the first part). The point, as I have now explained in several places, is that, "since program verification cannot guar- antee the performance of any program, it should not be pursued in the false belief that it can--which, indeed, might be entertained in turn as the 'ill-in- formed, irresponsible, and dangerous' dogma that my paper was intended to ex- pose" (CACM 32/3 (1989), p. 288). There is ample evidence that Martin has grasped neither the theoretical nor the practical issues involved here. In his message of 20 January 1990 at 15:11:42, Martin also maintains that, "these issues had been examined at some length in the formal methods com- munity. Had Dr Fetzer been conversant with the literature, he would have known it; had the reviewers been appropriately chosen, they would have called him on it." He repeatedly implies that I am ignorant, that the referees were incom- petent, and that the editors were irresponsible. Surely others besides Martin and his friends are capable of making such decisions. Indeed, Peter Denning's reply to complaints of this kind stands on its own without requiring endorse- ment from me (CACM 32/3 (1989), pp. 289-290). I have already explained my position on most of these matters (for example, CACM 32/3 (1989), pp. 288-289). For the benefit of those who cannot read or who do not understand what words mean, let me emphasize a few points that are relevant here. (1) The position under consideration is Hoare's position, as my article made entirely clear. Hoare is an important figure within the formal methods community. Not only is his position not trivial, it cannot be defended as justifiable or true. Yet it has been highly influential. (2) Not only does Martin not deny that Hoare has such a position, he even refers to it as "Hoare's Folly", characteristically substituting the use of labels or names for rational argument. Martin even agrees with me that Hoare's position is not acceptable and that program testing is required. (3) Surely in attacking some specific position, especially one that is well-defined, an author is not obli- gated to consider every possible alternative. Martin seems to be offended that neither I nor the referees nor the editors consulted him about these matters, as though he were some respository of truth about formal methods. Ler me close with a few personal observations. I have now received letters and email from around the world expressing diverse points of view. Some of these letters and messages have agreed with my position, while others have disagreed. With the possible exception of the "Gang of Ten", however, none of them has de- nied my right to examine these issues or the magazine's prerogatrive to publish it, apart from Charles Martin. His arrogant attitude and misleading contentions are not merely self-aggrandizing and obnoxious. They create the impression that there is a powerful clique within computer science that is unwilling to acknowl- edge the force of rational persuasion. From Martin's distorted remarks, I very much doubt that he has bothered to read the real debate over these issues in CACM (March, April, June, July, and Aug- ust) and Notices of the American Mathematical Society (September and December). There are real issues here that the community of the world cannot afford to mis-understand. For reasons such as these, I hope that other members of the Depart-ment of Computer Science at Duke University and of the profession as a whole will not be misled by infantile protestations masquerading as serious argument. James H. Fetzer
crm@romeo.cs.duke.edu (Charlie Martin) (02/26/90)
Okay, fine. Let's talk about these things some more. As long as we're
at it, I hope we can avoid the kind of ad hominem arguments that have
characterized Dr Fetzer's discussion so far.
Charles Martin's intemperate tirades concerning my position are
not even coherent. He belittles what he calls "Fetzer's Dilemma"
as irrelevant and insignificant, while simultaneously attacking
what he calls "Hoare's Folly" as relevant and significant. Since
Fetzer's Dilemma itself was a critique of Hoare's Folly, Martin's
position is not even consistent. Apparently, if he criticizes a
position, then it is important, but not if someone else does.
I *beg* your pardon. I believe if you actually read my notes, you
would have found that I referred to "Fetzer's Dilemma" specifically as
being a point that you had made. I believe, as you do, that expecting
absolute certainty of program verification is foolish; that is why one
of the "myths of verification" I identified in my postings was
"Hoare's Folly", the folly of believing that one can expect a proof of
properties of a program *text* to exactly correspond to the properties
of a realized program. Furthermore, I made the specific point in my
posting that you had identified this in your article, and that your
article led in part to my understanding of the folly described. I
believe my exact phrasing was "...but he has a point."
In other words, within those limits, I *agreed* with you. If what I
said is inconsistent, it can only be because your original points
were also inconsistent.
But, as I say, I only agree with you within limits. Consider the very
title of the article "Program verification: the very idea". The common
idiomatic meaning of the phrasing "the very idea" is understood as the
very idea so-and-so is foolish, meaningless, fallacious, nonsensical.
("Marry my daughter? Hmph. The very idea.")
My arguments concern whether computer science should be viewed as
a branch of pure mathematics or as a branch of applied
mathematics.
An excellent distinction that I believe was first stated in a letter
responding to your first article. As an *engineer* by orientation,
rather than a pure scientist or mathematician, I am most concerned with
the applied aspects although I find the pure math aspects attractive and
aesthetically pleasing.
The dilemma that I posed arises from the realization that purely
deductive reasoning cannot provide content about preformance for
any physical machine, so that if we want content about performance
of a physical machine, then purely deductive reasoning is not
enough. I do not deny that correctness proofs can be pursued as a
branch of applied mathematics, but their limitations--in principle
and in practice--must be clearly defined.
As examples of Martin's selective distortion of the real issues at
stake here, observe that, in his message of 20 January 1990 at
15:11:42, he maintains, "As a practical matter, the issues Fetzer
raised in his diatribe passing falsely as a technical article can
be largely ignored, both from the standpoint of engineering and
mathematically." Consider, however, what this person would have
you ignore (some of the most important consequences of my
position): "If one were to assume the execution of a program could
be anticipated with the mathematical precision that is
characteristic of demonstrative domains, then one might more
readily succumb to the temptation to conclude that decisions can
be made with complete confidence in the (possibly unpredictable)
performance of a complex causal system" (CACM 31/9 (1988), p.
1062). Perhaps this is a matter he wants to ignore, but the rest
of us do so at our peril.
Please consider carefully the phrasing that you quoted: "As a practical
matter, the issues... can be *largely* ignored...."
What I stated, apparently fairly clearly, was that in *many* areas of
programming, in many problem domains, and in many contexts, the issues
of correspondence between the mathematical model and the real-world
physical realization can be ignored. If we took a poll, I feel certain
that most fluent English speakers would agree that the phrasing I used
makes a careful effort NOT to claim absolutely that it can ALWAYS be
ignored.
Consider for example accounting programs: they are not life critical,
they are not performance critical, they do not have real-time demands
other than sufficient throughput. They usually have no asynchrony.
These programs are programs in which we are justified in assuming that
our mathematical model is "close enough" to the real world. The hazard
of being incorrect is small, the cost of complete testing is extremely
high, and the likelyhood that an error caused by an unpredictable event
(say a cosmic-ray alpha particle) will cause damage is extremely slight.
In life-critical systems, the situation is different. But
life-critical systems are being built today, WITHOUT a mathematical
basis, or worse, using mathematical methods based on assumptions that
we KNOW experimentally are flawed (cf. n-version programming, and
Avizenis' claims for it.) I doubt that either Dr Fetzer or I believe
that this situation is good, or that applying mathematical methods has
NO effect on correctness. (Certainly there is real evidence from
experiments that it does; if someone wants to believe otherwise in the
face of experimental evidence, I see it as a religious problem.)
In his message of 25 January 1990 at 18:07:15, he states that,
"Fetzer's argument is precisely that program proofs are flawed on
the face, that no proof can ever give insight or certainty to the
behavior of a real program on a real machine, because of the
distinction between the mathematical model and the real world."
Since part of what he says here is correct (the last part), it
gives a specious plausibility to the rest (the first part). The
point, as I have now explained in several places, is that, "since
program verification cannot guarantee the performance of any
program, it should not be pursued in the false belief that it
can--which, indeed, might be entertained in turn as the 'ill-in-
formed, irresponsible, and dangerous' dogma that my paper was
intended to expose" (CACM 32/3 (1989), p. 288). There is ample
evidence that Martin has grasped neither the theoretical nor the
practical issues involved here.
I'd say, rather, that there is ample evidence that Fetzer has neither
read nor understood what I said. As I pointed out above, I agreed, and
stated rather pithily, that mathematical reasoning alone was
insufficient, and that believing it was sufficient is folly. Hoare's
folly.
However, MY point, and the point made by many others who have responded
to Dr Fetzer, is that program verification can provide a sort of
*relative* guarantee: the likelyhood of defects in programs constructed
with proofs is very much smaller. Under the assumption that a trusted
stack has been constructed, the number of defects observed during
execution should approach zero, limited only by age or manufacturing
failures.
Furthermore, this relative guarantee is the ONLY kind of guarantee that
ANY engineering technique (or, for that matter, any scientific
exploration in the Logik der Forschung sense) can provide. All
physics and all engineering is based on the implicit or explicit
assumption that the mathematical model, the abstraction, that is
manipulated is sufficiently close to the behavior of the real world.
Engineers in other fields, such as civil engineers, regularly build
life-critical systems like bridges based on this assumption; the "formal
methods" of civil engineering consistently assume that the behavior of
the system is sufficiently well modelled by the behavior of the
mathematical models.
My best estimate -- I'm currently hoping to experimentally verify this
-- is that defects caused by errors in translation between
specifications and eventual executable code account for about 99.9
percent of all defects. I make the distinction here -- not an uncommon
one -- between *defects* as places where the code does not correctly
realize what was specified, and specification errors, where what was
built turns out not to meet the user's needs or desires, but does match
the specification.
In other words, only about one defect in a thousand occurs because the
compiler was wrong, the run-time system was buggy, the power glitched,
or the processor had an intermittent failure. Does Dr Fetzer claim that
verification gives NO guarantee that these sorts of translation errors
have been eliminated? If so, I think he's on very shaky ground,
logically; program proofs of this sort are precisely mathematical
theorems about string-to-string transformations under a formal system.
My experimental evidence is that simply performing hand proofs of the
design lowers the defect rate to the point where it is not observable on
the scale to which I've been able to apply the methods, building real
systems programs. Further, my experimentation suggests that hand-proven
programs serve as good firewalls which trap errors in unproven codes. I
hope to experimentally verify this on bigger problems; there is already
substantial experimental validation of similar techniques in the IBM
cleanroom experiments. But the experimental evidence is already pretty
clear: program verification has a substantial effect in removing defects
from codes.
In his message of 20 January 1990 at 15:11:42, Martin also
maintains that, "these issues had been examined at some length in
the formal methods community. Had Dr Fetzer been conversant with
the literature, he would have known it; had the reviewers been
appropriately chosen, they would have called him on it." He
repeatedly implies that I am ignorant, that the referees were
incompetent, and that the editors were irresponsible. Surely
others besides Martin and his friends are capable of making such
decisions. Indeed, Peter Denning's reply to complaints of this
kind stands on its own without requiring endorsement from me (CACM
32/3 (1989), pp. 289-290).
No, I didn't imply that you were ignorant, I stated it pretty baldly,
and will say it again. By your own statements, your article was based
on arguing against the foolish assertion of Hoare that testing was
completely unnecessary. However, this assertion is NOT mainstream in
the verification literature. In fact, I don't know of anyone who really
believes it in the verification community. But while I don't know of
anyone in the verification community who really believes it, I am aware
of a number of different projects specifically BASED on recognition that
program verification is only useful to the extent that the next layer
down is also proven. I've noted these before: consider the CLI trusted
stack, the analogous work at Odyssey, or Warren Hunt's verified
microprocessor work.
These projects would not be funded, active, or even interesting areas
of research IF it were not recognized that the issues of correspondence
between mathematical models and their physical realizations is a
significant problem. But your article doesn't refer to this research,
or the areas in the literature where these problems are discussed. In
fact, your article refers to no publications in the specific
verification literature that I recall. (If I am wrong, remind me of the
reference.)
To have failed to reference or consider a major body of literature on
the very topic of your paper is a failure in scholarship that wouldn't
be tolerated in "Introduction to Composition" classes at Duke; I see no
reason to feel kindly about it in a "technical" publication. However,
this isn't your field; if I wrote a paper which re-invented something
that Schopenhauer or Kant said, I'd be (marginally) proud of myself.
If I wrote a philosophy article which simply rehashed some old result
in, say, metaphysics, and it were published in a flagship refereed
journal of philosophy, I imagine you would feel it a scandal and a
shame.
The reason that journals are refereed is to catch this kind of error.
But your article wasn't caught in the refereeing process. The article
was apparently assigned to referees who were themselves not conversant
with the appropriate literature. Your article was then published. I
think this is a scandal and a shame.
I have already explained my position on most of these matters (for
example, CACM 32/3 (1989), pp. 288-289). For the benefit of those
who cannot read or who do not understand what words mean, let me
emphasize a few points that are relevant here.
(1) The position under consideration is Hoare's position, as my
article made entirely clear.
I wouldn't say it was entirely clear, since this was a topic of some
discussion for some time afterwards. Further, you did not reference
papers in which Hoare says "testing not required" most clearly; you
did reference papers in which Hoare makes explicit his simplifying
assumption that we can ignore hardware errors. It at least gave the
impression you had not even completely read the papers you cited.
Hoare is an important figure within the formal methods community.
Not only is his position not trivial, it cannot be defended as
justifiable or true. Yet it has been highly influential.
I doubt that even Hoare really believes "Hoare's Folly" -- careful
reading of his publications will certainly reveal plenty of times when
he adds a caveat to the effect that all these arguments assume the
hardware correctly executes the program.
In any case, your article is not titled "Hoare's assertion about
testing: the very idea". It refers to the entire field of program
verification, and assumes that Hoare speaks for that community in all
things. You claim that Hoare has been very influential, and you are
correct; however, in this area, the field had already advanced to the
point that we recognized Hoare was also WRONG, at least on this topic.
Unfortunately, you apparently did not pursue your research far enough
to recognize that the issue you raised was one that was already common
knowledge within the community.
(2) Not only does Martin not deny that Hoare has
such a position, he even refers to it as "Hoare's Folly",
characteristically substituting the use of labels or names for
rational argument.
Sure, sure, and when I refer to Russell's Paradox, that's also
substituting labels or names for rational argument. I stated a point,
then labelled it "Hoare's Folly" because (a) Hoare said it, and (b) it's
foolish.
Really, this is the worst sort of "argument by intimidation" and no
intellectually responsible philosopher would use it consciously. I
assume therefore it was a slip.
Martin even agrees with me that Hoare's position is not acceptable
and that program testing is required.
In other words, I agreed with you: what are you bitching about? I
didn't agree with you sufficiently strongly? Or that I dared to note
that you hadn't done your homework?
(3) Surely in attacking some specific position, especially one
that is well-defined, an author is not obligated to consider
every possible alternative. Martin seems to be offended that
neither I nor the referees nor the editors consulted him about
these matters, as though he were some repository of truth about
formal methods.
Well, in a word, yes, that is pretty much what offended me. Neither
you, nor the editors, nor the referees consulted me OR ANYONE ELSE WHO
WAS CONVERSANT WITH THE FIELD. I'm not one of the major voices in the
area; many of the major voices in the area responded along the same
lines as I have. (One of the major researchers in the field, John
Rushby, is an editor of the journal, and clearly the one to whom the
article should have been assigned.) It was a poor job of scholarship
and a poor job of refereeing that served the ACM very badly.
Let me close with a few personal observations. I have now
received letters and email from around the world expressing
diverse points of view. Some of these letters and messages have
agreed with my position, while others have disagreed. With the
possible exception of the "Gang of Ten", however, none of them has
denied my right to examine these issues or the magazine's
perogative to publish it, apart from Charles Martin.
For someone who inserts a sneer about those who read or understand what
words mean, you're playing pretty fast and loose here, bucko.
I did not claim that you had no right to examine these issues, only that
your examination recreated a well-known problem and claimed it as your
own creative effort. It may have been original from your point of view,
but it did not raise an unknown issue, nor did it clarify points that
were not already well known. You did not sufficiently explore the
existing literature; this is a sophomoric failure.
Nor did I claim that the magazine could not exercise the prerogative to
publish it. (Nor, actually, did the "Gang of Ten".) What they claimed,
and what I claim, is that for such a massive failure of scholarship to
have been promulgated in what is supposed to be -- what has in the past
been -- a major scholarly publication which claims to be the flagship
publication of the ACM was reprehensible and censurable.
You, Dr Denning, and CACM, can publish anything you like: I am not
obliged to respect poor work just because it is your right to publish
it.
His arrogant attitude and misleading contentions are not merely
self-aggrandizing and obnoxious. They create the impression that
there is a powerful clique within computer science that is unwilling
to acknowledge the force of rational persuasion.
I'm sorry, I must have missed a point here; was it "his arrogant
attitude" or "self-aggrandizing and obnoxious" that was the "rational
persuasion"?
I find I can't respond to your personal remarks adequately without
resorting to the sort of counter-insult that I gave up years ago.
"You're one." "You're another!" "So's your mama!" doesn't seem to me
to characterize the search for truth -- or the love of knowledge, which
is what philosophy is supposed to mean.
Charlie Martin (crm@cs.duke.edu,mcnc!duke!crm) djones@megatest.UUCP (Dave Jones) (03/01/90)
From article <3236@umn-d-ub.D.UMN.EDU>, by phil@umn-d-ub.D.UMN.EDU (Philosophy Dept): ... > > My arguments concern whether computer science should be viewed as a branch of > pure mathematics or as a branch of applied mathematics. > I can't tell you how it 'should be viewed'. (Through rose colored glasses?) But kind of job almost everybody with computer science degrees actually does for a living is neither mathematics nor science. It's mostly technical writing and engineering. (That's what I do, and my degree is master of _science_ in _mathematics_, for Pete's sake. Go figure.) Dave (Welcome to College - Here's Your High-Horse) Jones
crm@romeo.cs.duke.edu (Charlie Martin) (03/02/90)
In article <12178@goofy.megatest.UUCP.. djones@megatest.UUCP (Dave Jones) writes:
..From article <3236@umn-d-ub.D.UMN.EDU>, by phil@umn-d-ub.D.UMN.EDU (Philosophy Dept):
.....
..>
..> My arguments concern whether computer science should be viewed as a branch of
..> pure mathematics or as a branch of applied mathematics.
..>
..
..I can't tell you how it 'should be viewed'. (Through rose colored glasses?)
..But kind of job almost everybody with computer science degrees actually does
..for a living is neither mathematics nor science. It's mostly technical
..writing and engineering. (That's what I do, and my degree is master of
.._science_ in _mathematics_, for Pete's sake. Go figure.)
..
..
..
.. Dave (Welcome to College - Here's Your High-Horse) Jones
Sure, and what you've just described is a job in *software engineering*,
not *computer science*. Let's try to keep our terminology straight.
I'm with Fetzer on this: *computer science* is a kind of applied
mathematics: everything that we thiink of as being specific to computer
science is more or less mathematical in nature (sure, AI has a lot of
cognitive science/psychology involved, but that isn't specific to CS.)
But computer science != software engineering.
Charlie Martin (crm@cs.duke.edu,mcnc!duke!crm)