Re: Certified C compilers for safety-critical embedded systems

["Robert I. Eachus" <rieachus@comcast.net>]

Aatu Koskensilta wrote:

> The Halting Problems speaks about recursive functions. In order to make 
> applications of it to a real world situation, you have to be able to see 
> some things in the situation as being recursive functions. Otherwise 
> Halting Problem tells you nothing about the situation.

The Halting problem and G�del's proof are two sides of the same coin, at 
least in computer science.  The Halting problem is a constructive proof 
of G�del's proof.  In any language without partial recursive functions, 
the halting problem is trivial.  (All programs in that language always 
halt.)

If a language allows partial recursive functions, then it is Turing 
complete, and there is no general solution of the halting problem.  You 
can write a program that solves the halting problem correctly for some 
inputs.  But there are either inputs for which the program produces 
incorrect outputs, or there are inputs for which it never halts.  (And 
it is not difficult to prove that for some inputs, you won't be able to 
determine if the halting problem program will eventually halt.)

-- 
                                           Robert I. Eachus

"The war on terror is a different kind of war, waged capture by capture, 
cell by cell, and victory by victory. Our security is assured by our 
perseverance and by our sure belief in the success of liberty." -- 
George W. Bush