Xref: utzoo comp.ai:5610 comp.edu:2936 comp.object:770
Path: utzoo!utgpu!jarvis.csri.toronto.edu!cs.utexas.edu!uwm.edu!rpi!zaphod.mps.ohio-state.edu!uakari.primate.wisc.edu!aplcen!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: <1478@krafla.rhi.hi.is>
Date: 17 Jan 90 11:54:01 GMT
References: <16664@joshua.athertn.Atherton.COM>
Organization: University of Iceland
Lines: 25

From article <16664@joshua.athertn.Atherton.COM>, by joshua@athertn.Atherton.COM (Flame Bait):
> ...
> My last example points out a current problem with proving program correct.
> They must only use libraries which have been proven correct, must run on 
> an operating system which has been proven correct, and must use hardware
> which is proven correct.  All of this is impossible right now.

This is simply a problem of programming in general and has very little
to do with program proving.  When you prove something you generally
have to make some assumtions, in this case you would naturally assume
that the descriptions you have for library and system subroutines are
correct.  Where is the advantage of NOT proving your program correct?

> I'm serious about this challenge.  I hold that these program can not
> be specified in any kind of useful way, and that the set of programs 
> which can be proven correct is so small as to be uninteresting.

In that case the set of useful, trustworthy programs you CANNOT prove
correct must be large and interesting.  Would you care to give us some
examples?  Perhaps at the same time you could prove that they are
correct and trustworthy, but not provable!
-- 
Snorri Agnarsson		|  Internet:	snorri@rhi.hi.is
Taeknigardur, Dunhaga 5		|  UUCP:	..!mcvax!hafro!rhi!snorri
IS-107 Reykjavik, ICELAND