Xref: utzoo comp.ai:5511 comp.arch:13151 comp.databases:4617 comp.edu:2904 comp.object:736
Path: utzoo!utgpu!jarvis.csri.toronto.edu!cs.utexas.edu!usc!apple!apple.com!desnoyer
From: desnoyer@apple.com (Peter Desnoyers)
Newsgroups: comp.ai,comp.arch,comp.databases,comp.edu,comp.object
Subject: Re: Reasons why you don't prove your programs are correct
Message-ID: <6171@internal.Apple.COM>
Date: 13 Jan 90 01:03:58 GMT
Sender: usenet@Apple.COM
Organization: Apple Computer, Inc.
Lines: 20
References:<6158@internal.Apple.COM> <9237@medusa.cs.purdue.edu>

In article <9237@medusa.cs.purdue.edu> bls@cs.purdue.EDU (Brian L. Stuart) 
writes:
> Why do you feel that my proof was flawed?  I know its not as rigorous
> as it could be, but I don't thing its wrong.

Your proof was of the form "take program P and transform it into program 
P'. Verifying that P produces any output is the equivalent of solving the 
Halting Problem for P'". In other words, you showed that you could use a 
program that decides the Halting Problem to decide the verification 
problem. That isn't a particularly interesting result (since halting 
problem deciders can compute just about anything :-) - what we need to 
prove that the verifier cannot exist is to show that you can use the 
verifier to solve the halting problem.

Don't feel bad - I think I made the identical mistake on the net a year 
or two ago.

                                      Peter Desnoyers
                                      Apple ATG
                                      (408) 974-4469