Newsgroups: comp.ai
Path: utzoo!henry
From: henry@utzoo.uucp (Henry Spencer)
Subject: Re: Reasons why you don't prove your programs are correct
Message-ID: <1990Jan12.164806.601@utzoo.uucp>
Organization: U of Toronto Zoology
References: <25711@cup.portal.com> <1449@krafla.rhi.hi.is> <1990Jan11.015531.20996@world.std.com> <9220@medusa.cs.purdue.edu>
Date: Fri, 12 Jan 90 16:48:06 GMT

In article <9220@medusa.cs.purdue.edu> bls@cs.purdue.edu (Brian L. Stuart) writes:
>>The automatic program verification proponents lost. Perlis gave a good
>>talk on why...
>
>His arguments are significant and important practical considerations, but
>there is a more fundamental theoretical issue here....
>The upshot of this is that for any language...
>which is verifiable, there will be some programs that can be expressed
>on a Turing Machine which cannot be expressed in this language...

This is a complete red herring in the real world, however.  Inability to
verify arbitrary programs is irrelevant; programmers do not write arbitrary
programs.  It suffices to be able to verify the ones they do write.  The
practical problems dominate the theoretical ones here.
-- 
1972: Saturn V #15 flight-ready|     Henry Spencer at U of Toronto Zoology
1990: birds nesting in engines | uunet!attcan!utzoo!henry henry@zoo.toronto.edu