Subject: Re: Who's running your business?
From: Bernard Lang <Bernard.Lang@inria.fr>
Date: Tue, 30 May 2000 21:46:17 +0200



according to Curry and Howard, writing the proof, or writing the code
is essentially the same thing (isomorphism). Hence same difficulty.

And there are systems that allow codevelopement of both, or
translation from one into the other. Already used for some real
problems.

Bernard


On Tue, May 30, 2000 at 09:14:57AM -0700, Ian Lance Taylor wrote:
>    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

-- 
Bernard.Lang@inria.fr             ,_  /\o    \o/    Tel  +33 1 3963 5644
http://pauillac.inria.fr/~lang/  ^^^^^^^^^^^^^^^^^  Fax  +33 1 3963 5469
            INRIA / B.P. 105 / 78153 Le Chesnay CEDEX / France
         Je n'exprime que mon opinion - I express only my opinion
                 CAGED BEHIND WINDOWS or FREE WITH LINUX