Xref: utzoo comp.theory:855 sci.logic:888 sci.math:11711
Path: utzoo!attcan!utgpu!news-server.csri.toronto.edu!rutgers!usc!snorkelwacker!paperboy!husc6!m2c!umvlsi!dime!yodaiken
From: yodaiken@chelm.cs.umass.edu (victor yodaiken)
Newsgroups: comp.theory,sci.logic,sci.math
Subject: Re: Re^4: Question About the Four Color Proof
Message-ID: <16930@dime.cs.umass.edu>
Date: 15 Jul 90 14:48:16 GMT
References: <786@qusunu.queensu.CA> <9615@hubcap.clemson.edu> <1212@s8.Morgan.COM> <9649@hubcap.clemson.edu> <1233@s8.Morgan.COM>
Sender: news@dime.cs.umass.edu
Reply-To: yodaiken@chelm.cs.umass.edu (victor yodaiken)
Followup-To: comp.theory
Organization: University of Massachusetts, Amherst
Lines: 12

In article <1233@s8.Morgan.COM> amull@Morgan.COM (Andrew P. Mullhaupt) writes:
>In article <9649@hubcap.clemson.edu>, steve@hubcap.clemson.edu ("Steve" Stevenson) writes:
>> amull@Morgan.COM (Andrew P. Mullhaupt) writes:
>> 
>
>I am not aware of any reason that the computer part of the FCT proof
>should not be proven; what I mean here is that the source for the
>program can (and should) be equipped with a proof of partial correctness.

The reason appears to be that any such "proof", using current techniques,
would be less obviously correct than the program itself. Are there examples
of partial correctness proofs of substantive programs?