Path: utzoo!utgpu!jarvis.csri.toronto.edu!mailrus!cs.utexas.edu!wuarchive!decwrl!ucbvax!ucdavis!ucdavis.ucdavis.edu!windley From: windley@cheetah.ucdavis.edu (Phil Windley/20000000) Newsgroups: comp.edu Subject: Re: Reasons why you don't prove your programs are correct Message-ID: Date: 2 Feb 90 19:46:23 GMT References: <16479@joshua.athertn.Atherton.COM> <1455@krafla.rhi.hi.is> <16665@joshua.athertn.Atherton.COM> <10289@microsoft.UUCP> <19020@bellcore.bellcore.com> <10337@microsoft.UUCP> <3490@csccat.UUCP> <10417@microsoft.UUCP> Sender: uucp@ucdavis.ucdavis.edu Organization: UCD Robotics Research Lab Lines: 37 In-reply-to: jimad@microsoft.UUCP's message of 31 Jan 90 18:11:31 GMT I keep hoping to let this one drop, but people keep making comments that I just can't let go by. If you're tired of reading this, push "k" now. In article <10417@microsoft.UUCP> jimad@microsoft.UUCP (JAMES ADCOCK) writes: I think it is a gross distortion of reality to state that a program that in actually crashes is "correct" because it has been "proven" to be so. A real world customer tries running your "proven" correct spreadsheet and finds that your program crashes when other than trivial math expressions are requested of it. So said customer calls you up and you say: "I'm sorry sir, but that program *has* been proven correct!" BFD. No one who knows what verification is would ever say that anymore than Boeing would say in response to an airplane crash "I'm sorry, our computational fluid dynamics models don't predict that failure, so you're airplane must still be flying." Verification *IS NOT* about proving things about real computers and real programs running on real computers. It is about proving things about models of real computation. Now, if your contention is that nothing a model can tell me is worthwhile, then you'll never see any use in verification (or most of applied mathematics). I'm here to tell you that models are important and that the things that verification can tell you are important. I'm not going to claim that it will prove that a program works. Verification does not provide "knowledge" in the philosophical sense, it provides "justified true belief" which is the next best thing. -- Phil Windley | windley@cheetah.ucdavis.edu Division of Computer Science | ucbvax!ucdavis!cheetah!windley University of California, Davis | Davis, CA 95616 | (916) 752-6452 (or 3168)