Path: utzoo!censor!geac!torsqnt!news-server.csri.toronto.edu!cs.utexas.edu!usc!wuarchive!emory!hubcap!gatech!rutgers!cmcl2!kramden.acf.nyu.edu!brnstnd
From: brnstnd@kramden.acf.nyu.edu (Dan Bernstein)
Newsgroups: comp.object
Subject: Re: Proofs (was: Global program state.)
Message-ID: <7683:Jan501:13:0491@kramden.acf.nyu.edu>
Date: 5 Jan 91 01:13:04 GMT
References: <2474@motcsd.csd.mot.com> <10370@lanl.gov>
Organization: IR
Lines: 24

In article <10370@lanl.gov> jlg@lanl.gov (Jim Giles) writes:
> 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.

Well, one programmer not only published his correctness proofs as
models, but constructed his programs to be provable from the start.
He had so much faith in his correctness proofs that he didn't even test
the programs. As we all know, some of the code was buggy.

A flaw in a theorem brings the whole deck of cards tumbling down because
the *only* important thing in mathematics is truth. In contrast, as you
pointed out, a bug in a program generally doesn't render the program
useless. So it makes sense that the criteria for success in the two
disciplines should be different.

)  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.

Quite right.

---Dan