Path: utzoo!utgpu!news-server.csri.toronto.edu!rutgers!cs.utexas.edu!uunet!mstan!amull
From: amull@Morgan.COM (Andrew P. Mullhaupt)
Newsgroups: comp.theory
Subject: Re: Re^4: Question About the Four Color Proof
Message-ID: <1236@s8.Morgan.COM>
Date: 15 Jul 90 20:37:14 GMT
References: <786@qusunu.queensu.CA> <9615@hubcap.clemson.edu> <1212@s8.Morgan.COM> <16930@dime.cs.umass.edu>
Organization: Morgan Stanley & Co. NY, NY
Lines: 33

In article <16930@dime.cs.umass.edu>, yodaiken@chelm.cs.umass.edu (victor yodaiken) writes:
> 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. 
I cannot possibly see how. You cannot generally say in mathematics that
a result is obvious, and then expect a referee (who might not see it
as being so obvious) to let you off the hook for the proof. Thus, if the
proof of correctness can be had, what reason (which would be accepted
by a referee) can be given for its omission? If the proof _can_ be
given, why should it not? And how could a proof of a result make the
truth of that result less obvious?

> ... Are there examples
> of partial correctness proofs of substantive programs? 
I'm sure there are many, but this is irrelevant. Is the fact that the
classification of finite simple groups has a proof which spans thousands
of pages any reason to take that result on faith? One might argue on the
basis of a number of errors per journal page statistic, that the proof
is undoubtedly invalid, but is this any reason not to attempt it?
Mathematics may very well ponder the acceptability of proofs which 
require computers, but there is not much doubt about results which can
be proven conventionally - they should be.

Later,
Andrew Mullhaupt