Path: utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!uunet!mcsun!ukc!pyrltd!tetrauk!rick
From: rick@tetrauk.UUCP (Rick Jones)
Newsgroups: comp.object
Subject: Re: Proofs (was: Global program state.)
Message-ID: <1070@tetrauk.UUCP>
Date: 7 Jan 91 09:30:53 GMT
References: <2474@motcsd.csd.mot.com> <10370@lanl.gov>
Reply-To: rick@tetrauk.UUCP (Rick Jones)
Organization: Tetra Ltd., Maidenhead, UK
Lines: 40

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):
>> [...]
>> A program doesn't "work" because you (or somebody) thinks it works.  
>> A program "works" if it can be mathematically proven to work.  Experience
>> and operational time don't count.  This isn't like quantum physics where
>> observation decides the matter.  Empirical evidence doesn't enter into it.
>
>I must (at least partly) disagree with this.  A correctness proof is
>of similar complexity to the program it "proves" and is just as prone
>to errors as the program is.  (This possibility of error is present in
>_all_ mathematical proofs - which is why mathematics requires peer
>review and double-checking by other mathematicians.  No programmer
>I know of submits his correctness proofs to such scrutiny.)  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.

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.
(How many programs do you know that have work-rounds in them because code that
_should_ work according to the language definition in fact doesn't?)

This is almost like trying to prove mathematically that the universe works.  In
this case the boot is on the other foot;  the universe works by definition, it
is the job of mathematics and theoretical physics to find the methods to
describe mathematically what is known empirically to be true.

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.

-- 
Rick Jones
Tetra Ltd.  Maidenhead, 	Was it something important?  Maybe not
Berks, UK			What was it you wanted?  Tell me again I forgot
rick@tetrauk.uucp					-- Bob Dylan