Path: utzoo!attcan!uunet!lll-winken!brutus.cs.uiuc.edu!samsung!cs.utexas.edu!asuvax!ncar!mephisto!mcnc!duke!romeo!crm
From: crm@romeo.cs.duke.edu (Charlie Martin)
Newsgroups: comp.software-eng
Subject: Re: "Program Proving"
Message-ID: <18261@duke.cs.duke.edu>
Date: 16 Mar 90 17:00:07 GMT
References: <12326@goofy.megatest.UUCP>
Sender: news@duke.cs.duke.edu
Reply-To: crm@romeo.UUCP (Charlie Martin)
Organization: Duke University CS Dept.; Durham, NC
Lines: 57

In article <12326@goofy.megatest.UUCP> djones@megatest.UUCP (Dave Jones) writes:
>
>   [ I suppose that you program-provers, once you have proved you program,
>     are going to prove that the proof is correct, yes? No? ]
>
>
>Anecdote 1:
>
>....A couple of months later a bug manifested
>itself. No, it wasn't due to a typo in the coding -- and not a compiler-bug,
>either. The proof contained a mistake corresponding to a mistake in the code.
>
Yup, that happens.  Just as in ...

>Anecdote 2:
>
> .... Of course, my advisor checked it carefully, as
>supposedly did the jury, but I guess there is some possibility that I too
>overlooked something. It is a very knotty bit of business, that.
>

>Now consider that both of those faulty proofs underwent much closer scrutiny
>than my little program-proof of anecdote-1 did -- years of scrutiny --
>more than ANY program-proof is ever likely to undergo, yet each was incorrect.
>
>The point is, if you think that doing a formal proof is a good way to budget
>your system test time, by all means go ahead. Just don't think it proves
>anything conclusively. You better run lots of carefully selected test-cases
>too.

I don't *think* a formal proof is a good way to budget test time, I have
evidence from controlled studies and anechdotal evidence that says it
is.  Even better, I have a strong suspicion that the proof can direct
the testing to improve it.

But let's just look at the opposite side of this statement:  "If you
think that a formal proof is a good way to establish a mathematical
statement, by all means go ahead.  Just don't think it proves anything
conclusively.  You'd better do lots of carefully-selected examples too."

As a mathematician, this ought to immediately strike you as something
between "a little off" and "of course; any mathematically literate
person knows that you should make sure that a simple example ought to
work too."  (Although there are those horror stories about the person
who one way or another had a counter-example to his main theorem proven
during his defense.)  The point of program proving (IM philosophical O)
is that it establishes the basis on which predictions can be made,
against which actual tests can be performed, to raise the certainty of
correctness into the realm of "inductive" or "abductive"
demonstration.

If you want to look into this point further, I can mail you the
Canonical Flame War between Jim Fetzer and myself.  If that threat
doesn't put you off, nothing will.....


Charlie Martin (crm@cs.duke.edu,mcnc!duke!crm)