Xref: utzoo comp.ai:5488 comp.arch:13114 comp.databases:4598 comp.edu:2891 comp.object:721
Path: utzoo!utgpu!jarvis.csri.toronto.edu!cs.utexas.edu!samsung!sol.ctr.columbia.edu!cica!iuvax!purdue!bls
From: bls@cs.purdue.EDU (Brian L. Stuart)
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: <9220@medusa.cs.purdue.edu>
Date: 11 Jan 90 20:19:21 GMT
References: <25711@cup.portal.com> <1449@krafla.rhi.hi.is> <1990Jan11.015531.20996@world.std.com>
Reply-To: bls@cs.purdue.edu (Brian L. Stuart)
Followup-To: comp.ai
Organization: Department of Computer Science, Purdue University
Lines: 33

In article <1990Jan11.015531.20996@world.std.com> bzs@world.std.com (Barry Shein) writes:
>
>The automatic program verification proponents lost. Perlis gave a good
>talk on why, it went something like:
>

His arguments are significant and important practical considerations, but
there is a more fundamental theoretical issue here.

1)  No program can be verfied to be correct unless it is verified that it
    produces the correct output.
2)  In verifying the correctness of the output, one verifies the existence
    of the output.
3)  Assume that a program exists that can verify the existence of output.
    Now create a pre-processor that takes as input a program and produces
    as output the same program except that it halts after every output.
    (The construction of such a program is left as a excercize for the
    reader :-)  Now the combination of this pre-processor with the assumed
    verifier is a program which will detect whether or not a program halts.
    Hopefully, everyone recognizes that this is impossible according to the
    halting theorem, so our assumption of a program that can verify the
    existence of output must be false and by 1) and 2) we cannot have
    a program that verifies the correctness of programs in general.

The upshot of this is that for any language or programming methodology
which is verifiable, there will be some programs that can be expressed
on a Turing Machine which cannot be expressed in this language or
methodology.  When you ask for verifibility, you ask to sacrifice
Turing-compatability.  Be careful what you ask for, you may get it.

Brian L. Stuart
Department of Computer Science
Purdue University