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

   Date: Tue, 30 May 2000 07:27:46 -0600
   From: ksvhsoft@xmission.com (Kevin S. Van Horn)

   > Maybe it's time to start paying attention to
   > provably correct software again.

   And maybe the time is just right for it now.  Critics of the notion of proving
   software correct have long argued its infeasibility on the basis that software
   development lacked the "social process" behind the acceptance of proofs in
   mathematics.  It seems to me that bazaar-style development might just provide
   that "social process".

   Another thought: proofs of correctness are most useful in tricky pieces of
   code that are difficult to adequately test.  Code for synchronizing concurrent
   threads fits the bill perfectly.  Now that multi-threaded code is becoming
   more common, might correctness proofs for synchronization become a standard
   tool for the software engineer instead of an academic subject?

I've seen two main problems with correctness proofs.

The first is that doing the proofs is not significantly easier than
writing the code.  Automated theorem provers can help, but you still
need to write the correct assertions.  Assertions are a great way to
focus thought when you are writing the code, but they are much less
effective when they have to be tied together as the basis for a formal
proof.

The second is that proof methods that I am aware of essentially
require writing the code twice: once for the code itself and once for
the proof system.  Nothing forces the proof system to match the actual
code.  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.

The notion of correctness proofs is an attractive idea, and it is a
good program development technique.  However, unless you are actually
writing in a logic programming language, I think that the only way to
prove that software is correct is to simulate every possible branch
condition while using executable assertions.  In a preemptive
multi-threaded programming environment, any instruction can branch, so
this can be a tedious chore.

I won't even get into proving the correctness of the compiler, the
supporting libraries, the operating system, or the hardware.

I don't think a free software bazaar helps correctness proofs.
Proving that code is correct is, if anything, more difficult than
writing it in the first place.  I don't think there are a lot of
people out there able and willing to provide the social process you
mention.  But perhaps I misunderstand your suggestion.

Ian