steve@hubcap.clemson.edu ("Steve" Stevenson) (07/13/90)
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
steve@hubcap.clemson.edu ("Steve" Stevenson) (07/13/90)
aaron@grad2.cis.upenn.edu (Aaron Watters) writes: >What makes you think that the program is any more or less proven >than other parts of this or other proofs? The non-computer piece seems to have been check for whatever. However, the program has not been subjected to such scrutiny ( the deMillo argument against proofs). > The algorithm is certainly ... [possibility of an implementation mistake] > I'd say this is much less likely than the possibility of an ordinary >mathematical nonsequitur in the main part of the proof, > especially since the algorithm has been reimplemented and rerun. And rederived, also, or just recoded? -- =============================================================================== Steve (really "D. E.") Stevenson steve@hubcap.clemson.edu Department of Computer Science, (803)656-5880.mabell Clemson University, Clemson, SC 29634-1906
aesop@milton.u.washington.edu (Jeff Boscole) (07/14/90)
----------------------- 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" ?? :-) :=: