Xref: utzoo comp.ai:5609 comp.edu:2935 comp.object:769
Path: utzoo!utgpu!jarvis.csri.toronto.edu!cs.utexas.edu!uunet!mcsun!hafro!isgate!krafla!snorri
From: snorri@rhi.hi.is (Snorri Agnarsson)
Newsgroups: comp.ai,comp.edu,comp.object
Subject: Re: Reasons why you don't prove your programs are correct
Message-ID: <1479@krafla.rhi.hi.is>
Date: 17 Jan 90 12:04:23 GMT
References: <16665@joshua.athertn.Atherton.COM>
Organization: University of Iceland
Lines: 25

From article <16665@joshua.athertn.Atherton.COM>, by joshua@athertn.Atherton.COM (Flame Bait):
> In article <1455@krafla.rhi.hi.is> snorri@rhi.hi.is (Snorri Agnarsson) writes:
>>And a third group (including myself) thinks it means you can put
>>assertions in your code and in your interfaces and carefully
>>try to see to it that those assertions are true at each time point.
> I would group you into my second group.  The assertions are checked
> both statically and dynamically.  By the way, I agree that this is
> good programming practice and I do it myself, but it is not "proving
> a program correct".  I consider it part of defence in depth.

I usually just check the assertions statically myself, unassisted,
and the assertions are simply comments in the program text,
not executable statements.
Arguing about whether this is a proof or not will not get
us far.  I claim this is a proof in the usual mathematical
sense.  Some people seem to think a proof is not a proof
until a proof checker has validated it.  I disagree.
Validation by a proof checker would give me more confidence
in a proof, that's all. 
I agree that this is part of defence in depth, so perhaps
we only disagree on the definition of the word "proof".
-- 
Snorri Agnarsson		|  Internet:	snorri@rhi.hi.is
Taeknigardur, Dunhaga 5		|  UUCP:	..!mcvax!hafro!rhi!snorri
IS-107 Reykjavik, ICELAND