Re: Certified C compilers for safety-critical embedded systems

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

Aatu Koskensilta wrote:

> So your original statement
> 
>  [any compiler for a resonable language] either does not accept some
>  legal programs, accepts some illegal  programs, or never halts for some
>  inputs
> 
> is correct if the reasonable language we're speaking about is Ada. I 
> think that, say, Haskell is a reasonable language, and the above does 
> not hold for it - the type system is decidable -, but perhaps you find 
> Haskell unreasonable.

No, I used Ada as an example because everyone here should be familiar 
with it, and I am VERY familiar with where the bodies are buried, since 
I helped bury some of them.

The proper way to describe my contention is probably:

All realizable implementations of any programming language are finite. 
(This is because the hardware is a good, but finite, imitation of a 
Turing complete system.)

If a language definition imposes limitations more restrictive than those 
imposed by the hardware, the programming language is finite.  This is 
harder to do than it seems.  For example, Java goes to extremes to 
insist that everything is a 32-bit quantity, including pointers.  But it 
doesn't prevent say a 64-bit implementation from mapping larger physical 
addresses into 32-bit pointers.  As a simple example, an implementation 
could insist that all addressable constructs begin on a 64-bit boundary 
and use 64-bit word addresses rather than 8-bit byte addresses.  (Some 
Java implementations do use word addresses in pointers.)

If the language is Turing complete, but the compiler runs on real 
hardware, then you can't use the compiler to tell the difference between 
physical limitations and cases where it is undecideable whether a 
program is illegal.  You have to rely on analysis to recognize the later 
case.

In particular, for Ada 83 I demonstrated a real case where the legality 
of a program was undecideable, and two compilers gave different (but 
correct) answers.  Given time I can probably find similar cases for all 
Turing complete programming languages, including the usual suspects of 
Fortran, Cobol, C, and Ada 95.  (C++ is so easy it seems like cheating.)

But my real point is that compiler developers can't just wish away 
G�del's proof, and they don't.  Good compilers are always careful to 
distinguish between cases where the compiler can decide that a program 
is illegal and cases where a submission exceeds the capabilities of the 
implementation, but may or may not be illegal.  The example I gave was a 
rare case where a compiler could reach a conclusion about an 
undecideable case based on the run-time behavior of the code that 
compiler would generate.  (And where two compilers were known to make 
different choices for the same hardware.)

-- 
                                           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