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-16 20:13:37 PST Path: archiver1.google.com!news2.google.com!news.maxwell.syr.edu!newshub.sdsu.edu!elnk-nf2-pas!elnk-pas-nf1!newsfeed.earthlink.net!pd7cy1no!shaw.ca!border1.nntp.ash.giganews.com!border2.nntp.sjc.giganews.com!border1.nntp.sjc.giganews.com!nntp.giganews.com!local1.nntp.sjc.giganews.com!nntp.comcast.com!news.comcast.com.POSTED!not-for-mail NNTP-Posting-Date: Fri, 16 Jan 2004 22:13:36 -0600 Date: Fri, 16 Jan 2004 23:13:35 -0500 From: "Robert I. Eachus" User-Agent: Mozilla/5.0 (Windows; U; Windows NT 5.0; en-US; rv:1.4) Gecko/20030624 Netscape/7.1 (ax) X-Accept-Language: en-us, en MIME-Version: 1.0 Newsgroups: comp.lang.ada Subject: Re: Certified C compilers for safety-critical embedded systems References: <0F6Nb.1623$Tt.642@reader1.news.jippii.net> In-Reply-To: Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 8bit Message-ID: NNTP-Posting-Host: 24.34.214.193 X-Trace: sv3-KMENbm+ZL9NXFCUT9w2Yodr3YfXdH0t/GttoyPCRAcQ29rsS3lRKmG1U6qPHjzH3FqvNlvCkx1TSrkG!2b7nRCHhssVFsyZDiX7zBuAnXtH74xc3efLJzS61PH1lu82HH8/vAG0Wxg2nLw== X-Complaints-To: abuse@comcast.net X-DMCA-Complaints-To: dmca@comcast.net X-Abuse-and-DMCA-Info: Please be sure to forward a copy of ALL headers X-Abuse-and-DMCA-Info: Otherwise we will be unable to process your complaint properly X-Postfilter: 1.1 Xref: archiver1.google.com comp.lang.ada:4480 Date: 2004-01-16T23:13:35-05:00 List-Id: David Starner wrote: > In this sense, Ada compilers don't implement a Turing-complete language, > nor are they written in a Turing-complete language. Modern computers, like > any computer in the real world, are merely finite state machines, as a > true Turing machine requires infinite storage, so G�del's proof doesn't > apply. Yes, all Ada implementations implement a finite subset of Ada. But, to some extent the limitations are a function of the hardware, not of the compiler. The usual way of talking about it is that the triplet of (hardware, operating system, compiler) defines a subset of Ada that can be compiled. (Although in reality, you need to consider both the host and target hardware and OSes.) In theory, you could write an Ada compiler that attempted to implement (full) Ada, and would only be limited by the actual hardware. If you did that then you could talk about what G�del's Proof has to say about the compiler as a device for recognizing Ada. In practice we ignore the fact that addresses are of a static size, since that size is often larger than any realistic implementation can support. (In other words many compilers today support 64-bit addresses. I doubt that there is 2**64 bytes of memory connected to the Internet. Of course, we will probably get there in a few years. But compiling programs that need 2**64 bytes of memory when being compiled will still take longer than most people are willing to wait.) The point is though, that G�del's proof does apply. We know that no matter how much memory we make available to a compiler, there are some legal programs the compiler can't compile. The compiler could accept illegal programs instead, but we try very hard to avoid that. It is G�del that tells us we have to accept one or the other condition. -- 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