Path: utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!yale!cmcl2!lanl!jlg
From: jlg@lanl.gov (Jim Giles)
Newsgroups: comp.object
Subject: Proofs (was: Global program state.)
Message-ID: <10370@lanl.gov>
Date: 4 Jan 91 18:37:36 GMT
References: <2474@motcsd.csd.mot.com>
Organization: Los Alamos Natl Lab, Los Alamos, N.M.
Lines: 26

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.

I think your mistake here is picking on the word "work". A program
works if it performs acceptably _most_ of the time.  If the cost of
fixing the last few bugs in a program is greater than the cost of
living with those bugs in place - don't bother fixing them.  In a
practical world, _only_ empirical evidence matters.  By your definition
of "work", _none_ of the UNIX environment does so.  Come to think of
it, maybe you're right after all :-).

J. Giles