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: What's Right and Wrong About Charles Martin's Position Keywords: correctness, validation, testing, program verification Message-ID: <3237@umn-d-ub.D.UMN.EDU> Date: 25 Feb 90 22:38:16 GMT Organization: U of Minnesota-Duluth, Information Services Lines: 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