🚀 go-pugleaf

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