Path: utzoo!mnetor!uunet!husc6!mit-eddie!ll-xn!ames!pasteur!agate!garnet.berkeley.edu!csm
From: csm@garnet.berkeley.edu
Newsgroups: comp.software-eng
Subject: Re: correctness proofs (was Re: Complexity Measures)
Message-ID: <6764@agate.BERKELEY.EDU>
Date: 29 Jan 88 00:10:10 GMT
References: <5874@sol.ARPA> <30176UH2@PSUVM> <1273@lznv.ATT.COM> <1958@svax.cs.cornell.edu>
Sender: usenet@agate.BERKELEY.EDU
Reply-To: bks@ALFA.berkeley.edu.UUCP ()
Organization: University of California, Berkeley
Lines: 27
Summary: Who watches the watchman

In article <1958@svax.cs.cornell.edu> siegel@svax.cs.cornell.edu (Alexander Siegel) writes:
>In article <1273@lznv.ATT.COM> psc@lznv.ATT.COM (Paul S. R. Chisholm) writes:
>>In article <30176UH2@PSUVM>, UH2@PSUVM.BITNET (Lee Sailer) writes:
>>>...
>>> PROGRAM CORRECTNESS PROOFS:  All the work on this seems to require the
>>>...
>>It's quite impossible to prove most software "correct", either because
>>it's not correct (no smiley)...
>>...
>....  The biggest efforts are being made in automatic progarm verification...
> In five years ...
>-- 

It will take more than five years to prove the automatic program verifier
software is "correct" (also no smiley). However, using "assertive"
comments is a lot of help to you and to other savvy programmers who might
want to muck around with your code.

			-- Brad Sherman

P.S.  If employers could imagine longer time spans than "until the
next shareholders' meeting" they might understand that by giving programmers
(sorry, Software Engineers) offices instead of cubicles, they will eventually
INCREASE profits.

P.P.S Has anyone seen a study of the effect on productivity of (gasp)
increasing vacation time.