Path: utzoo!utgpu!jarvis.csri.toronto.edu!mailrus!uflorida!mephisto!mcnc!duke!romeo!crm
From: crm@romeo.cs.duke.edu (Charlie Martin)
Newsgroups: comp.software-eng
Subject: Re: "Correct" IS UNDEFINED!
Message-ID: <17272@duke.cs.duke.edu>
Date: 2 Feb 90 14:54:29 GMT
References: <1278@oravax.UUCP> <39400060@m.cs.uiuc.edu>
Sender: news@duke.cs.duke.edu
Reply-To: crm@romeo.UUCP (Charlie Martin)
Organization: Duke University CS Dept.; Durham, NC
Lines: 17

In article <39400060@m.cs.uiuc.edu> render@m.cs.uiuc.edu writes:
>
>No one (except maybe you) thinks that "proving a program correct" means
>proving absolutely, positively that there is not a single (no, not even
>one) error in a program.  

Would that this were true.  This is, unfortunately, just about exactly
what I've spoken of as "Hoare's Folly."  Hoare's argument for it depends
on his (usually implicit) assumption that the only REAL program is the
mathematical argument written on paper; he explicitly ignores executino
concerns.  Unfortunately he also makes the assumption the the True and
Good Programmer will never make mistakes.  Thus the presumption (and
ghod is it presumptive!) that proven programs need not be tested.

If this were better recognized, perhaps Fetzer's Dilemma would have been
recognized as the straw man it really is.
Charlie Martin (crm@cs.duke.edu,mcnc!duke!crm)