🚀 go-pugleaf

In article <9220@medusa.cs.purdue.edu> bls@cs.purdue.EDU (Brian L. Stuart) 
writes:
>[flawed proof that program verification is impossible.]

Try this one instead. Given a program V that will verify whether or not 
program P run on input I will produce output O. We can transform P by 
deleting all output statements and having it output a single value O' 
before it halts. [ie. transform P() to P'(),print(O') where P'() is P() 
with all print statements deleted.] V(P',I,O') will then determine whether 
or not the output of P'(I) is O', which is equivalent to determining 
whether P(I) halts.

Therefore V cannot exist. However, this result isn't as useful as it 
seems. First, there are important classes of programs where V is 
computable, even if it is not computable on all programs. Second, program 
verification often means proving whether or not P (the program) is 
equivalent to P' (the specification), which is a different problem 
entirely. (although probably not computable in the general case.)

                                      Peter Desnoyers
                                      Apple ATG
                                      (408) 974-4469