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 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-14 08:11:07 PST Path: archiver1.google.com!news2.google.com!fu-berlin.de!news.eunet.no!uio.no!newsfeed.kolumbus.fi!not-for-mail From: Aatu Koskensilta Newsgroups: comp.lang.ada Subject: Re: Certified C compilers for safety-critical embedded systems Date: Wed, 14 Jan 2004 18:32:46 +0200 Organization: Elisa Internet customer Message-ID: References: <0F6Nb.1623$Tt.642@reader1.news.jippii.net> NNTP-Posting-Host: 212-246-60-38.adsl.tpo.fi Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 8bit X-Trace: phys-news1.kolumbus.fi 1074096665 5510 212.246.60.38 (14 Jan 2004 16:11:05 GMT) X-Complaints-To: abuse@kolumbus.fi NNTP-Posting-Date: Wed, 14 Jan 2004 16:11:05 +0000 (UTC) User-Agent: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.2.1) Gecko/20030225 X-Accept-Language: en-us, en In-Reply-To: Xref: archiver1.google.com comp.lang.ada:4404 Date: 2004-01-14T18:32:46+02:00 List-Id: Alexandre E. Kopilovitch wrote: > Aatu Koskensilta wrote: > > >>>Why do you call that reference to G�del's proof "curious"? >> >>Because it seems flat out wrong. That >> >> [any compiler for a resonable language] either does not accept some >> legal programs, accepts some illegal programs, or never halts for some >> inputs >> >>does not in any sense > > > Hm, _any_? How can you know about _any_ sense? There may be a sense of which > you just aren't aware (for example, a sense of _real_ general-purpose > programming languages and _real_ requirements for _really_used_ compilers > for those languages -;). Then the impossibility follows from some constraints imposed by these "reality" requirements, whatever they are, and not from G�del's theorem (or the undecidability of the Halting Problem, which seems more appropriate here). The only way to get from undecidability of the Halting Problem to the conclusion is to insist that "reasonable" languages must be compile-time Turing-complete. I know of no language in wide use today that would meet this requirement. >>follow from G�del's proof. > > > It can't formally follow - just because the quoted statement is not formal - > it couples the formal part with informal part, and the latter refers to a hard > reality. So, the statement isn't a logical conclusion, it is an opinion about > relationship between a particular logical construct and a piece of reality. It isn't. There's a very clear sense in which the above claim can be taken to be about recursive functions - in which case all sorts of considerations about hard relaity are obviously irrelevant -, in this case about recursive functions that perform transformations on strings. To re-iterate what I've said above: such a transformation is non-recursive just in case it is (or can be made in a suitable manner) a (recursive) encoding of a non-recursive function. In hard reality there are very few correct compilers if any, but this has nothing to do with G�del's theorem or its proof. -- Aatu Koskensilta (aatu.koskensilta@xortec.fi) "Wovon man nicht sprechen kann, daruber muss man schweigen" - Ludwig Wittgenstein, Tractatus Logico-Philosophicus