🚀 go-pugleaf

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