Article View: comp.ai
Article #8731Re: Reasons why you don't prove your programs are correct
From: David H. West
Date: Fri, 12 Jan 1990 05:51
Date: Fri, 12 Jan 1990 05:51
14 lines
1307 bytes
1307 bytes
In article <9220@medusa.cs.purdue.edu> bls@cs.purdue.edu (Brian L. Stuart) writes: >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. I'd be more than happy to sacrifice completeness of the verifier provided that soundness is maintained (i.e. it's never wrong when it says "Verified", though it may say "Don't Know" sometimes), and provided that the verifier is at least as clever as a global optimizing compiler. -David West dhw@iti.org
Technical Details
Message-ID:
<4784@itivax.iti.org>Path:
arc1-ca.pugleaf.net!utzoo!attcan!uunet!ns-mx!ceres!zaphod.mps.ohio-state.edu!wuarchive!cs.utexas.edu!mailrus!sharkey!itivax!dhwReferences:
<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
Path: arc1-ca.pugleaf.net!utzoo!attcan!uunet!ns-mx!ceres!zaphod.mps.ohio-state.edu!wuarchive!cs.utexas.edu!mailrus!sharkey!itivax!dhw From: dhw@itivax.iti.org (David H. West) Newsgroups: comp.ai Subject: Re: Reasons why you don't prove your programs are correct Message-ID: <4784@itivax.iti.org> Date: 12 Jan 90 05:51:50 GMT References: <25711@cup.portal.com> <1449@krafla.rhi.hi.is> <1990Jan11.015531.20996@world.std.com> <9220@medusa.cs.purdue.edu> Reply-To: dhw@itivax.UUCP (David H. West) Organization: Industrial Technology Institute Lines: 14