Re: Certified C compilers for safety-critical embedded systems

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

David Starner wrote:

> Because it's wrong. An assembler is a simple compiler; where does a
> simple assembler which merely looks up mnemonics in a table run into
> G�del's proof? There is a Turing complete language with one instruction:
> subtract and jump if negative. So you have a bunch of lines like SJN %0 %1
> %2, where you subtract %1 from %0 and jump to %2 if negative. I see no
> point where a compiler from this language into Ada or x86 assembly would
> not accept some legal programs, accept any illegal programs, or not halt.

No, an assembler is NOT a simple compiler, at least in the generally 
accepted sense of the term.  A compiler parses context free languages. 
The assembler you hypothesized is capable of being recognized by a 
finite state machine instead of a push-down automata.

> So obviously reasonable doesn't mean Turing-complete. But if it doesn't,
> where does G�del come in? It seems implausible that every "reasonable"
> language is uncompilable. A Basic subset with integer variables A-Z and
> POKE, PEEK, assignment, +, -, *, /, =, <, > and an if/then/goto construct
> is about equal to some real life Basics, so in some sense is reasonable.
> Maybe my imagination is failing me, but I fail to see why G�del's proof
> is involved in compiling this to any other reasonable language. I doubt
> the compiler language would have to even be Turing complete.

Okay, let's try again.  All major programming languages cannot be 
recognized by a finite state machine.  If a language can be recognized 
by a FSM, it is not subject to G�del's Proof.  Assuming away the 
features of a context free grammar that cause the problem, and then 
saying it doesn't exist is silly.  Do you know of any regularly used 
programming languages that don't require PDAs to recognize them?  I 
don't, and I spent decades creating and maintaining compilers and 
programming languages.  (A lot of compilers use LL1 grammers and 
"recursive descent" parsers.  In that case the call stack serves as an 
implicit push-down structure for the parser.  Parsers which use LALR or 
even LR(k) grammars usually use an explicit push-down automata.)

> No completely optimizing compiler can exist for any reasonable programming
> language, but that's not what he said. Perhaps most languages in existence
> run into G�del problems on simple compilation, but I would hesitate to
> say that all "reasonable" languages fall into that category.

I didn't hesitate, and I said it.  Incidently there are some languages 
which are normally interpreted that can be recognized by FSMs.  But they 
are not normally considered to be programming languages, general purpose 
or otherwise.

All this should be standard material in any graduate level course on 
computability.

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