Article View: comp.ai
Article #8726Re: Reasons why you don't prove your programs are correct
From: Henry Spencer
Date: Fri, 12 Jan 1990 16:48
Date: Fri, 12 Jan 1990 16:48
17 lines
1342 bytes
1342 bytes
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
Technical Details
Message-ID:
<1990Jan12.164806.601@utzoo.uucp>Path:
arc1-ca.pugleaf.net!utzoo!henryReferences:
<25711@cup.portal.com> <1449@krafla.rhi.hi.is> <1990Jan11.015531.20996@world.std.com> <9220@medusa.cs.purdue.edu>Show Full Headers
Complete Article Headers
Newsgroups: comp.ai Path: arc1-ca.pugleaf.net!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