Subject: Re: who's running your business?
From: (Kevin S. Van Horn)
Date: Wed, 31 May 2000 21:27:39 -0600

Ian Lance Taylor writes:

> I was trying to argue that proving code correct is not a silver bullet
> either

I would certainly agree here.  Perhaps I didn't make myself clear.  I view
program proof as a useful tool for certain difficult situations.  Proofs don't
replace testing and code review; rather, they complement and augment these.

> As it happens, I believe that the most effective way to find bugs is
> code reviews by other programmers.

But some things are too difficult to analyze by just walking through the code
and simulating its execution in your head.  That's when an informal
correctness proof -- preferably embedded as comments in the source -- can be
very, very useful.  The code review can then include reviewing the proof.  You
know that your proof has sufficient detail when all of the reviewers
understand it and find it convincing.  I believe that IBM calls this the
"clean room" method.