On Thu, Apr 17, 2008 at 3:21 AM, Eleanor McHugh
<eleanor / games-with-brains.com> wrote:
>  Now the Halting Problem is fascinating because it's very simple in
> conception: given a program and a series of inputs (which in Godel's terms
> comprises a mathematical system and a set of axioms) determine whether or
> not the program will complete. Turing proved that in the general case this
> problem is insoluble, and not only does this place an interesting
> theoretical limitation of all software systems but it also applies to
> sub-programs right the way down to the finest grain of detail. Basically
> anytime a program contains a loop condition the Halting Problem will apply
> to that loop.
>
>  So in essence we're left with a view of software development in which we
> can never truly know if a program is correct or even if it will halt.

In general, proofs around Turing machines only applies with an
infinite length tape - in other words, about a computer with infinite
memory.

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.

Eivind.