On 17 Apr 2008, at 10:29, Eivind Eklund wrote:
> The Halting proof only proves that there exists programs that we can't
> prove halting about, not that it isn't possible to prove things around
> some programs.
>
> The Goedel proof is about complete logical systems; in the case of a
> computer program, we are working with a system where we have other
> formalisms under it that's providing axioms that we don't prove, just
> assume.
>
> In the absence of hardware failure (something we of course can't prove
> and is a problem in the real world), we can trivially prove halting
> for a lot of cases.  E.g, the simple program "halt" halts.  halt if
> true halts.  halt if 1 == 1 would generally halt, assuming no
> redefinition of ==.  An so on.
>
> I appreciate and respect your general contributions in this thread; I
> just couldn't let this particular argument stand, as it confuse people
> about what the theorems say.

I fully agree with you that for degenerate cases the halting problem  
is trivial. Unfortunately these tend to be the exceptions in real  
world programs as opposed to the rule. For safety-critical systems  
where unexpected halting is a run-time exception that needs to be  
handled I think it is highly relevant, although it can rapidly become  
a red herring if viewed out of context.


Ellie

Eleanor McHugh
Games With Brains
http://slides.games-with-brains.net
----
raise ArgumentError unless @reality.responds_to? :reason