Path: utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!samsung!usc!snorkelwacker.mit.edu!mit-eddie!uw-beaver!cornell!oravax!ian
From: ian@oravax.UUCP (Ian Sutherland)
Newsgroups: comp.object
Subject: Re: Proofs (was: Global program state.)
Message-ID: <1987@oravax.UUCP>
Date: 10 Jan 91 04:43:50 GMT
References: <2474@motcsd.csd.mot.com> <10370@lanl.gov> <1070@tetrauk.UUCP>
Reply-To: ian@oravax.odyssey.UUCP (Ian Sutherland)
Organization: ORA Corporation, Ithaca, New York
Lines: 47

In article <1070@tetrauk.UUCP> rick@tetrauk.UUCP (Rick Jones) writes:
>In article <10370@lanl.gov> jlg@lanl.gov (Jim Giles) writes:
>>From article <2474@motcsd.csd.mot.com>, by lance@motcsd.csd.mot.com (lance.norskog):
>>I must (at least partly) disagree with this.  A correctness proof is
>>of similar complexity to the program it "proves"

Not always.  Sometimes, especially in the case of proofs that are
constructed in a mechanical theorem proving environment, the proof's
complexity is much greater!  If reasonable use is made of decisions
procedures, it can be less.

>>and is just as prone
>>to errors as the program is.

This is not so relevant if you don't see program proofs as iron-clad
guarantees that the program will never disappoint you with what it
does.  If a proof, correct or incorrect, points out an error, then
it's been of use.

>>To be sure,
>>correctness proofs identify _some_ bugs in the program and are valuable
>>as debugging tools.  But such proofs aren't _replacements_ for all the
>>other debugging tools.

Amen.

>They also only get you part of the way.  Suppose you have proved your program
>correct, this can only be in terms of the language(s) in which it is written
>and possibly specified.  This still doesn't prove that it will work in practice
>unless you have also proven correct the compiler, assembler, linker (and
>whatever other levels of translation are involved), as well as the CPU design,
>microcode (if a CISC machine), and indeed the entire hardware environment.

I don't have statistics at my finger tips for this, but I believe the
vast majority of programming errors occur at the source code level,
and are not due to errors in compilers, hardware, etc.

>If my program "works", the fact that I can't prove it is a failure of the
>proving methods, not a failure of the program.

Many a program has seemed to "work" for a very long stretch of time
before bugs were discovered.  Some of these bugs would have been found
by proof.
-- 
Ian Sutherland				ian@oracorp.com

Sans peur