Xref: utzoo comp.theory:851 sci.logic:885 sci.math:11694
Path: utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!wuarchive!mit-eddie!uw-beaver!milton!aesop
From: aesop@milton.u.washington.edu (Jeff Boscole)
Newsgroups: comp.theory,sci.logic,sci.math
Subject: Re: Re^6: Question About the Four Color Proof
Summary: Beef
Keywords: computer proof
Message-ID: <5045@milton.u.washington.edu>
Date: 13 Jul 90 18:53:03 GMT
References: <1212@s8.Morgan.COM> <4997@milton.u.washington.edu>
   <9663@hubcap.clemson.edu>
Organization: University of Washington, Seattle
Lines: 26

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

>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.

In regards "whole class of cases" -- this appears to be a mathematical
   issue and not one for computer science per se...

In regards "compiler, op. sys. machine" etc. (and I think that you meant
   a "whole class of cases" might be missed for -these- reasons), suppose
   I wrote the operating system -and- the compiler -and- the program
   which did the checking of an enormous quantity of cases, then included
   detailed descriptions of the operation system, the compiler, the machine
   and the program -along- with the detailed mathematical description of
   the proof.  After satisfying these five criteria, are there any others
   that might be required to fulfill the notion of "knowledge" ??  :-)


:=: