Subject: Re: Who's running your business?
From: Ian Lance Taylor <ian@airs.com>
Date: 30 May 2000 23:03:09 -0700

   Date: Tue, 30 May 2000 22:37:54 -0600
   From: ksvhsoft@xmission.com (Kevin S. Van Horn)

   I'm not proposing to prove correctness for everything.  Nor am I proposing a
   100% formal, machine-checkable proof.  I rarely do correctness proofs myself,
   but every once in a while I run up against something tricky where it's very
   difficult to be sure you have it right by just doing operational reasoning.
   That's when a correctness proof, or mathematical derivation of the algorithm,
   can be indispensable.

I agree.  I do the same thing.

   > It's easy to write code which appears to be proven correct,
   > only to discover that the code does not actually meet the assertions.
   > This is most likely in cases such as the multi-thread synchronization
   > which you mention, in which error cases arise very rarely so
   > executable assertions are no guarantee of correctness.

   It seems to me that you're getting proofs and testing mixed up.  The whole
   point of a proof is that it doesn't matter how rare the case is, you still
   have to account for it or your proof is incomplete.  And often it's a
   lot easier to see that you're missing a piece of your proof than it is to
   write exhaustive tests.

My point is that nothing forces the proof and the code to be
identical.  Even if the proof is correct, the code may still be
incorrect.  I mentioned executable assertions because many people use
those as part of proving code to be correct, in an attempt to make the
proof and the code as identical as possible.

I personally don't find it any easier to see that I am missing a piece
of a proof than to write exhaustive tests.  The most common case in
which I use proofs is to make sure that complex data structure
manipulations maintain invariants.

Ian