Xref: utzoo comp.theory:846 sci.logic:882 sci.math:11679
Path: utzoo!attcan!uunet!convex!texsun!newstop!sun-barr!cs.utexas.edu!usc!zaphod.mps.ohio-state.edu!swrinde!emory!hubcap!steve
From: steve@hubcap.clemson.edu ("Steve" Stevenson)
Newsgroups: comp.theory,sci.logic,sci.math
Subject: Re^6: Question About the Four Color Proof
Keywords: computer proof
Message-ID: <9663@hubcap.clemson.edu>
Date: 12 Jul 90 20:36:03 GMT
References: <9615@hubcap.clemson.edu> <1212@s8.Morgan.COM> <4997@milton.u.washington.edu>
Organization: Clemson University, Clemson, SC
Lines: 28

aesop@milton.u.washington.edu (Jeff Boscole) writes:


>In article <9649@hubcap.clemson.edu>
>    steve@hubcap.clemson.edu ("Steve" Stevenson) writes:

>>... however my interest is in the fact that a computer program is
>>involved. In the philosophical sense, has FCT been `proven' if it has an

>Forgive me for being dense....  I've attempted to understand these issues
>thru Philosophy of Science classes and so forth....  Precisely -where- is
>the beef with a "proof by an (unverified.by.hand.calculation) computer
>program?"

The beef is that no one can verify (by hand or otherwise) that the program
does precisely what it is supposed to do. How do you know that there isn't
a whole class of cases which were missed? By the time the compiler, op. sys.
and the machine get done with it, how do you know that the program
actually run is `the same' as the one originally intended?

See the long running battle in computer science over this issue.


-- 
===============================================================================
Steve (really "D. E.") Stevenson           steve@hubcap.clemson.edu
Department of Computer Science,            (803)656-5880.mabell
Clemson University, Clemson, SC 29634-1906