From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00,FREEMAIL_FROM autolearn=ham autolearn_force=no version=3.4.4 X-Google-Language: ENGLISH,ASCII X-Google-Thread: 103376,a00006d3c4735d70 X-Google-Attributes: gid103376,public X-Google-ArrivalTime: 2004-01-13 21:00:53 PST Path: archiver1.google.com!news2.google.com!news.maxwell.syr.edu!newsfeed.mathworks.com!wn11feed!worldnet.att.net!bgtnsc04-news.ops.worldnet.att.net.POSTED!not-for-mail From: David Starner Subject: Re: Certified C compilers for safety-critical embedded systems User-Agent: Pan/0.14.2 (This is not a psychotic episode. It's a cleansing moment of clarity. (Debian GNU/Linux)) Message-Id: Newsgroups: comp.lang.ada References: MIME-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 8bit Date: Wed, 14 Jan 2004 05:00:52 GMT NNTP-Posting-Host: 12.72.183.225 X-Complaints-To: abuse@worldnet.att.net X-Trace: bgtnsc04-news.ops.worldnet.att.net 1074056452 12.72.183.225 (Wed, 14 Jan 2004 05:00:52 GMT) NNTP-Posting-Date: Wed, 14 Jan 2004 05:00:52 GMT Organization: AT&T Worldnet Xref: archiver1.google.com comp.lang.ada:4379 Date: 2004-01-14T05:00:52+00:00 List-Id: On Wed, 14 Jan 2004 01:18:48 +0300, Alexandre E. Kopilovitch wrote: > Aatu Koskensilta wrote: > >> > Anyone who works on compiler front end and language definitions has to >> > be ready to dance with G�del, decidability issues and the whole >> > nine yards. ANY compiler for a reasonable programming language, and >> > even for some unreasonable ones runs right straight into G�del's >> > proof. It either does not accept some legal programs, accepts some >> > illegal programs, or never halts for some inputs. >> >> Where do you get this curious idea about G�del's proof? > > Why do you call that reference to G�del's proof "curious"? 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. 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. 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.