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

On Tue, May 30, 2000 at 07:27:46AM -0600, Kevin S. Van Horn wrote:
> 
> > 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".

see for example http://www.monde-diplomatique.fr/en/1998/01/12freesoft
(paragraph before last)

 but other authors must have said it.

> 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?

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