Path: 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

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