Path: utzoo!attcan!uunet!wuarchive!brutus.cs.uiuc.edu!zaphod.mps.ohio-state.edu!sol.ctr.columbia.edu!cica!iuvax!purdue!bls
From: bls@cs.purdue.EDU (Brian L. Stuart)
Newsgroups: comp.ai
Subject: Re: Reasons why you don't prove your programs are correct
Message-ID: <9236@medusa.cs.purdue.edu>
Date: 12 Jan 90 21:09:31 GMT
References: <25711@cup.portal.com> <1449@krafla.rhi.hi.is> <1990Jan11.015531.20996@world.std.com> <9220@medusa.cs.purdue.edu> <1990Jan12.164806.601@utzoo.uucp>
Reply-To: bls@cs.purdue.edu (Brian L. Stuart)
Organization: Department of Computer Science, Purdue University
Lines: 52

In article <1990Jan12.164806.601@utzoo.uucp> henry@utzoo.uucp (Henry Spencer) writes:
>In article <9220@medusa.cs.purdue.edu> bls@cs.purdue.edu (Brian L. Stuart) writes:
>>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.

Several people have raised this point.  (I just picked a short article to
follow up.)  I don't dispute it, at least not absolutely.  However, I
do think a few considerations are in order.
1)  Any language or metholodogy which has enough power to allow the
    expression of a Turing Machine simulator must be Turing compatible
    (defined by:  any program that can be expressed on a Turing Machine
    can also be expressed in the compabible language).  Now, I'm not
    a language designer, but I have trouble imagining a language that
    cannot allow the expression of a TM simulator and still be useful,
    since a TM simulator is a very simple program and bears some
    similarity to other useful programs.
2)  Any verifiable language or methodology must be limited relative
    to a TM (as discussed in previous messages).  If you give me such
    a language or methodology, my first reaction is to ask "What are
    its limits?"  That's why I said one should be careful in asking
    for verifiability.  It's a good thing when it can be achieved,
    but it implies limitations that need further study.

Interestingly, there are a couple of good theoretical objections that
I haven't seen yet.  First, a computer is NOT a TM.  It has finite memory.
Such a system is theoretically no more powerful than a Finite Automaton.
Consequently, the halting theorem doesn't really apply to computer
programs.  Unfortunatly, from this point of view, the verifier must
be a machine much larger than the verifiee which can be a bit of a
problem in practice.  The second objection is that if we specify a
time limit in the verification process, then the proof of the halting
theorem (at least all that I've seen) falls apart.  I don't know if
anyone has shown whether the halting problem on programs with time
limits is solvable.  Also this is beginning to sound alot like the
old batch systems where jobs needed a card that specified how long
it was to run.  Even if it needed only another second, it was
unceremoniously discharged from service.

Again, I'm not against verifiers (although for me, they would make
programming alot less fun).  However, there are serious theoretical
implications, and it remains to be shown whether or not these
implications carry over to the practicle domain.

Brian L. Stuart
Department of Computer Science
Purdue University