Path: utzoo!utgpu!jarvis.csri.toronto.edu!cs.utexas.edu!usc!zaphod.mps.ohio-state.edu!uakari.primate.wisc.edu!uflorida!mephisto!mcnc!duke!romeo!crm
From: crm@romeo.cs.duke.edu (Charlie Martin)
Newsgroups: comp.software-eng
Subject: Re: What's Right and Wrong About Charles Martin's Position
Keywords: correctness, validation, testing, program verification
Message-ID: <17813@duke.cs.duke.edu>
Date: 26 Feb 90 17:40:06 GMT
References: <3237@umn-d-ub.D.UMN.EDU>
Sender: news@duke.cs.duke.edu
Lines: 85



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)