Path: utzoo!utgpu!jarvis.csri.toronto.edu!rutgers!umn-d-ub!phil
From: phil@umn-d-ub.D.UMN.EDU (Philosophy Dept)
Newsgroups: comp.software-eng
Subject: Re: Reasons why you don't prove your programs are correct
Keywords: verification, testing, validation, Charles Martin
Message-ID: <3236@umn-d-ub.D.UMN.EDU>
Date: 24 Feb 90 23:27:09 GMT
Organization: U of Minnesota-Duluth, Information Services
Lines: 85

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