phil@umn-d-ub.D.UMN.EDU (Philosophy Dept) (02/26/90)
After reviewing your USENET messages of the last month or so, I want to state, at least in part, why I find your public behavior to be so obnoxious. In the process, perhaps you will be able to appreciate why I am reacting so strongly. (1) In your article 1392, for example, you responded to Robert Munch with der- ison and abuse. "Oh, crap", you say, belittling his argument. "This is the most assinine (sic) argument that I've seen proposed." Messages like this one lead me to suggest that you really should not call people names that you cannot even spell. It creates the impression that you are not merely abusive but also asinine. And I know you would not want to be accused of relying on ad hominems. (2) In your article 1338, for another, you refer to my publication in CACM as a "diatribe". I wonder if you have consulted a dictionary lately as to the mean- ing of that word. According to Webster's New World Dictionary (1988), "diatribe" means a bitter, abusive criticism or denunciation. This is a better descrip- tion of your message than it is of my article. It would be rather difficult for you to find even one passage of my article that supports you. Go back and take a look. And you are doing all this over a world-wide net! (3) In your article 1427, for a third, you describe my position as that of a "straw man". As I have previously observed, you implicitly contradict yourself in doing so, since you combine your diatribe against me with an assault on Pro- fessor Hoare (who is a far more decent human being than some of his critics). But your bitter denunciation of my CACM article only makes sense if Hoare is right! Otherwise, I am right in criticizing him and you are wrong in criticiz- ing me. Why is this something that you are unable to understand? (4) Your problem, I believe, is confusing my critique of a specific position on program verification with an attack upon the program verification community. I was attacking Hoare's position; I was not attacking the community itself. Look at the first sentence, the first paragraph, and the first few pages I wrote. You seem to be unable to distinguish between the specific position that was under consideration and the heterogeneous views of a diverse community. Surely I am entitled to critique Hoare's position without being responsible for also assess-ing whatever 1001 other voices may have said in other places. (5) I just know how proud you would have been during the debate at ACM CSC 90 when I quoted some of your heroes from Computational Logic. Yes, I cited J. Strother Moore himself, for example, when he remarked, "In a verified system one can make the following startling claim: if the gates behave as formally modeled, then the system behaves as specified" (Journal of Automated Reason- ing 5/4 (1989), p. 409). As I observed, this should come as welcome news to the sports car manufacturers, the cruise missile commanders, and the space craft managers. (It is a startling claim, especially considering its source!) (6) I also quoted another luminary from the field whom you must also admire, William R. Bevier, when he observed, "The key to our approach to systems ver- ification is the use of formally-defined abstract machines" (Journal of Auto- mated Reasoning 5/4 (1989), p. 427). These machines, he explains, are explic- itly defined as functions in Boyer-Moore logic, which you endorse. But the problem remains of establishing that our abstract models are adequate to the physical world that they are intended to represent. This leads directly to Fetzer's Dilemma by a route that is too obvious to need review. (7) I think your problem is one of public relations. You are evidently upset because I criticized a position to which I referred as "program verification". You admit that the position I have criticized deserved to be criticized, yet you insist that I am attacking a "straw man". This leads me to ask you to go back and reread the Viewpoint by Dobson and Randell (CACM 32/4 (1989), pp. 420-422). They believe that your field suffers from a gap between its public image and its private reality. They describe the situation that you are in. (8) The questions at stake here, by the way, are not technical points of pro- gram verification. They are problems in the theory of knowledge. It would be far more appropriate, I believe, if you were to simply admit that what I have said is correct about the positon that I have attacked, but that you--and many others--represent other positions. Surely the opinions of other commentators, including Dobson and Randell, suggest that these other views, which you are now so eager to advance, have not been much in evidence until this debate arose. (9) A crucial point. Yet another interesting equivocation enters the picture at this juncture. The team of Ardis and Gries, who were presumably defending formal methods in software engineering at ACM CSC 90, explicitly DISAVOWED the thesis that, "Formal methods of program verification should be the principal methodology of software engineering in each of its phases for assessing the reliability of software systems." If you agree with them and with me in deny- ing that this proposition is true, perhaps we are not that far apart, after all. (10) When you express your views on these matters in the future, however, it might be very helpful to carefully distinguish between "formal proofs", "proof sketches", and mere "deductive reasoning". No one would deny that deductive reasoning is indispensable to program construction, but that is hardly an im- portant position. I know that you think that the vast literature to which you constantly refer makes these things completely clear. I do not believe there exists any single unified and coherent position which your "community" shares. Since I have consistently maintained that program verifiction can exist as a branch of applied mathematics (CACM 31/9 (1988), pp. 1059-1060; CACM 32/8 (19- 89), pp. 920-921; and Notices of the AMS 36/10 (1989), p. 1353), it is very hard to see why you are carrying on such an abusive tirade. So quit bitching. James H. Fetzer
crm@romeo.cs.duke.edu (Charlie Martin) (02/27/90)
In response to at least one question, the reason I continue arguing with
Dr Fetzer is (1) I've got more dedication to the old business about the
pursuit of truth than I do sense, and (2) I really do think the issues
are important and significant.
Now, I'd like to summarize my position briefly (believe it or not):
(1) I recognize the distinction Dr Fetzer makes between deductive
knowledge and scientific or inductive knowledge. He was right about
the distinction, as I've said all along. However, it was not a new
idea in the community or a new distinction.
(2) Hoare has said in print that once a program is proven tests are no
longer needed. (See e.g. pg 319 of Hoare and Jones _Essays in
Computing Science_, in the paper "Programming is an Engineering
Profession".) I believe this is folly.
(3) However, I do not believe that Dr Fetzer's paper and its publication
represented good or responsible scholarship, for the following
reasons:
(a) It presented no new information. The issue he drew was one that
is well-known in the literature. It makes no mention of other
considerations of the same problem is widely-accessible
publications. (examples follow.)
(b) After several re-readings, it still appears to me to state that
program verification per se is fatally flawed, not just Hoare's
position with reference to testing. My previous posting notes
several reasons why I believe it gives that impression.
I promised examples. Here are two, drawn from the books I can reach
with my left hand from my desk.
From "Mechanical proofs about computer programs", Donald I Good, in
Hoare and Shepherdson _Mathematical Logic and Programming Languages_, pp
70-71. (Prentice-Hall, 1985)
"However, there are several reasons why a program that has been
proved within the Gypsy environment may not behave exactly as
expected. First, the formal specifications may not describe exactly
the expected behavior of the program. Secondly, the formal
specification may not describe all of the aspects of program
behavior. Thirdly, invalid lemmas may have been assumed without
proof. Finally, either the verification environment, the compiler,
the Gypsy run-time support or the hardware might malfunction.
....These sources of error are cited not to belittle the potential
of a scientific basis for software engineering but to make clear
that the formal, mathematical approach offers no absolutes."
From _Formal Methods of Program Verification and Specification_, Berg et
al., pg 36. (Prentice-Hall 1982)
"Another limitation arises from the necessarily abstract view we take
of program semantics and the corresponding distance that exists
between a formally verified program and the physical manifestation
of its behavior. .... The functioning of the hardware is a physial
process, subject to the laws of nature. Ultimately, then, the
confidence we have in the correctness of a program depends upon our
belief that the proper physical actions will result. As a result,
there is no "bottom line" at which we can show that executing a
program is guaranteed to produce the desired effect. The best we
can do is show that programs are correct with respect to their
execution on some abstract machine, which we model with a deductive
system. The _truth_, as opposed to the validity, of the theorems in
the deductive system depends upon the proper implementation of the
program semantics--that is, of the abstract machine--by hardware and
software."
I believe these two quotes show that Dr Fetzer's position was well-
understood and widely recognized long before his paper was published.
Charlie Martin (crm@cs.duke.edu,mcnc!duke!crm) crm@romeo.cs.duke.edu (Charlie Martin) (02/27/90)
Quick repsonses:
(1) It's commonly considered good form either to completely quote, or to
indicate elision by ellipsis. In this case, I beleive what I wrote was
"Oh, crap. I'm sorry, but this is the most assinine...." I apologize
abjectly for sullying the discussion with the word crap, even though I
apologized in line.
W.r.t. "assinine". Oh my goodness, I made a spelling mistake.
(2) "Diatribe: a bitter and abusive criticism or denunciation;
invective." I calls'em as I sees'em. No apology.
(3) "Straw man: one set up as an opponent to be easily defeated or
refuted." As I've shown, the position you refuted is one widely known,
understood, and widely discussed in the literature to be false. You
then proceeded to refute it. This is a straw man. No apology.
My criticism has always been not that you are wrong, but that your
point is as widely known as the fact that ice melts. Taken at the
epistomological level you apparently intend, the same argument calls
into question all applied math that is used to predict physical law, or
else can be summarized as "our predictions are only as good as our
understanding."
(4) You may be right. If so, I'm not alone in this. You could have
made the fact that you intended only to disagree with Hoare's position
much clearer, as evidenced by the fact that *many* people have
misunderstood you the same way.
(5) I don't think I follow your point. I have no doubt that J said
that; I agree with it, and it appears to agree with you substantial
point. But when I took intro philosophy courses years ago, I learned
something they called the "principle of substitution": that one could
evaluate a questionable argument by recasting it using other words from
the approproate grammatical classes. For example, recasting in terms of
a sports-car manufacturer:
"In a mathematically analyzed engine, one can make the following
startling claim: if the components behave as modelled, then the
engine will behave as predicted."
Do you disagree with this statement? It strikes me as tautological.
(6) If you haven't grasped by now that I am completely aware of the
distinction between formal system and physical realization, nothing
further I can say will convince you. I notice you seem to have
given up the position that the name "Fetzer's Dilemma" was
derogatory.
(7) It is the fact that verification has public relations problems; I
don't think you have been very helpful with them. But many people
believe in astrology; it isn't astronomy's major purpose to dissuade
them.
(8) As my previous posting demonstrated, they have been widely known; so
widely known that I doubt many people thought there was any point in
rehashing them. It is just unfortunate that you were not widely
enough read in the literature to realize this.
(9) You know philosophy better than to actually think that what you
state is an equivocation. It is a denial of a thesis that was badly
stated.
"Formal methods of program verification should be the principal
methodology of software engineering in each of its phases for
assessing the reliability of software systems."
You should have heard the moaning in the local office of CL inc when
this thesis was published. Who came up with the phrasing?
In any case, I do agree that this is an unsupportable thesis. Had
it been stated "Formal methods should be the principle
methodology...." I would be closer to agreeing with it, as I would
expect that included Markov methods and queueing theory.
(10) I doubt that in as new and diverse a field as verification, you
could get agreement on when to have lunch, much less on technical
details. But I suspect that the point "corrrectness of the final
system depends on how well our model of the realization models
physical reality" comes as close as any. As familiarity with the
literature would have revealed.
Charlie Martin (crm@cs.duke.edu,mcnc!duke!crm) sean@castle.ed.ac.uk (S Matthews) (02/27/90)
Would Fetzer and Martin move their mutual loathing society to alt.mud.slinging and let the rest of us get on with more intelligent debate. The original debate was interesting. Your personal hate mail is not. Go and stand in opposite corners, both of you until you cool off. Sean