🚀 go-pugleaf

From article <25711@cup.portal.com>, by mmm@cup.portal.com (Mark Robert Thorson):
> There was an excellent article about 10 years ago in CACM on this.
> I believe the title was "The Social Process and Proofs of Program
> Correctness".  This article marked the death of program verification;
> feelings which had echoed in the halls of academia and industry
> for more than a decade were expressed in a clear form in print,
> and from that point on the "conventional wisdom" was that program
> verification was a dead-end for research.  In retrospect, it's hard
> hard to see why this wasn't obvious from the very beginning.

I have not read this article and I must confess it is not obvious
at all to me that verification is dead.  Perhaps automatic program
verification is dead, that would not surprise me, but I still believe
all programmers should prove their programs while they write them,
even if the proofs are only for their own consumption.  I believe
this is especially important for large projects with many procedures.
To be able to maintain a large program you need to know the following
for each procedure:

	1)	Under what circumstances is it allowed to call the
		procedure? (those are the procedures preconditions)

	2)	Assuming it is allowed to call the procedure, what
		will it's effect be?  (postconditions)

It is astonishing how often large projects are done without documenting
the above information.  

-- 
Snorri Agnarsson		|  Internet:	snorri@rhi.hi.is
Taeknigardur, Dunhaga 5		|  UUCP:	..!mcvax!hafro!rhi!snorri
IS-107 Reykjavik, ICELAND