Path: utzoo!utgpu!jarvis.csri.toronto.edu!mailrus!cornell!oravax!ian
From: ian@oravax.UUCP (Ian Sutherland)
Newsgroups: comp.ai
Subject: Re: Re^2: Reasons why you don't prove your programs are correct
Message-ID: <1245@oravax.UUCP>
Date: 12 Jan 90 21:02:22 GMT
References: <25711@cup.portal.com> <1449@krafla.rhi.hi.is> <1990Jan11.015531.20996@world.std.com> <548@tci.bell-atl.com> <1990Jan12.030424.1397@world.std.com>
Reply-To: ian@oravax.odyssey.UUCP (Ian Sutherland)
Organization: Odyssey Research Associates, Ithaca, New York
Lines: 25

In article <1990Jan12.030424.1397@world.std.com> oravax!cornell!batcomputer!rpi!zaphod.mps.ohio-state.edu!swrinde!cs.utexas.edu!yale!mintaka!bloom-beacon!bu.edu!bu-cs!xylogics!world!bzs bzs@world.std.com (Barry Shein) writes:
>The halting problem states (very roughly) "There exists at least one
>program who's halting conditions cannot be determined".

This a little TOO rough for me.  To speak roughly, but a little less
roughly than above, the unsolvability of the halting problem states
that there is no recursive procedure which will take a program P and an
input I and tell you whether P halts if started on I.  For a given
recursive procedure, there is always some P and some I such that the
given recursive procedure gives the wrong answer.  The particular P
and I depend on the recursive procedure, they are not fixed for all
time.

>Computer science education makes far too much of this interesting
>observation and seems to leave people forever without hope that any
>automatic examination of a loop can be fruitful (e.g. in a debugging
>compiler.)

Yes, I agree wholeheartedly.  In fact, I think the recursive
unsolvability of the halting problem has little to do with the
practical concerns of computing or verification.
-- 
Ian Sutherland		ian%oravax.uucp@cu-arpa.cs.cornell.edu

Sans Peur