Path: utzoo!attcan!uunet!lll-winken!brutus.cs.uiuc.edu!rpi!zaphod.mps.ohio-state.edu!usc!ucsd!ucbvax!bloom-beacon!eru!luth!sunic!mcsun!ukc!edcastle!sean
From: sean@castle.ed.ac.uk (S Matthews)
Newsgroups: comp.software-eng
Subject: Re: "Program Proving"
Message-ID: <2872@castle.ed.ac.uk>
Date: 16 Mar 90 11:10:56 GMT
References: <12326@goofy.megatest.UUCP>
Reply-To: sean@castle.ed.ac.uk (S Matthews)
Organization: Edinburgh University Computing Service
Lines: 45

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:
>
>I often think about "invariant relations" and such when I'm programming, but
>only once in the eleven years that I've been doing software engineering full
>time have I written out a formal proof of a piece of production code. (Stop me
>if you've heard this one.) The thing was made-to-order for a formal proof.
>It was a tricky hash-table algorithm. It was so tricky, that I figured I
>better prove it, so I did. A fellow worker had checked over my proof with me,
>verifying that it was correct. 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.
>
>Anecdote 2:
[deleted, makes same point]

You are not making a distinction between `formal' and `usual
mathematical': a formal proof is a machine checkable structure in the
class of deductions in a formal theory.  THe option of a mistake is not
there (of course your theory may be inconsistent---but I humbly suggest
that this is *unlikely*, or the proof checker may be buggy, but proof
checkers are very simple programs). 

>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 agree, but you had also better be careful about what you call a formal
proof. 

Sean

P.S.  there are good examples of *formal* proof systems around too, and
not just for the sort of weenie math that is needed for program
verification.  Try Cornell's NuPRL system for instance.  (A friend of
mine produced a proof of the finite version of Ramsey's theorem in it,
and I would say that that has been checked a great deal more thoroughly
than if Euclid, Archimedes, Newton, Gauss, Euler and Hilbert refereed it
together).