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=unavailable autolearn_force=no version=3.4.4 X-Received: by 10.107.166.69 with SMTP id p66mr4314576ioe.85.1511403344157; Wed, 22 Nov 2017 18:15:44 -0800 (PST) X-Received: by 10.157.42.99 with SMTP id t90mr972681ota.5.1511403344075; Wed, 22 Nov 2017 18:15:44 -0800 (PST) Path: eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!feeder.eternal-september.org!news.kjsl.com!usenet.stanford.edu!i6no4083811itb.0!news-out.google.com!193ni7431iti.0!nntp.google.com!d140no4083547itd.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail Newsgroups: comp.lang.ada Date: Wed, 22 Nov 2017 18:15:43 -0800 (PST) In-Reply-To: Complaints-To: groups-abuse@google.com Injection-Info: glegroupsg2000goo.googlegroups.com; posting-host=2601:191:8303:2100:1874:7b05:762e:e9fa; posting-account=fdRd8woAAADTIlxCu9FgvDrUK4wPzvy3 NNTP-Posting-Host: 2601:191:8303:2100:1874:7b05:762e:e9fa References: <2fca0f38-833e-485d-9a38-febcdd507bb1@googlegroups.com> User-Agent: G2/1.0 MIME-Version: 1.0 Message-ID: Subject: Re: More reliable compilers (of some programming langauges) than GNAT From: Robert Eachus Injection-Date: Thu, 23 Nov 2017 02:15:44 +0000 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Xref: feeder.eternal-september.org comp.lang.ada:49087 Date: 2017-11-22T18:15:43-08:00 List-Id: On Tuesday, November 21, 2017 at 8:19:28 PM UTC-5, Randy Brukardt wrote: =20 > Seriously, though, the idea of a bug-free compiler for any non-trivial=20 > programming language is rather laughable. >=20 > It's possible that the application of proof tools to compilers will impro= ve=20 > their quality (especially possible in the back-ends), but there is always= =20 > going to be the problem of adequately expressing the correct result. One= =20 > would have to have a completely formal description of the programming=20 > language -- but then how would one prove that there are no bugs in that= =20 > formal description (most likely written in a language that hardly anyone= =20 > would understand)? You have a problem that essentially is an infinite=20 > regress - you're always going to end up at some point with a description= =20 > that cannot be proved correct (and is too complex to ensure correct). I'm going to be the grinch here and invite G=C3=B6del to the party. The nam= e GNAT was chosen as a subtle reference to the fact that no compiler can be= proven to completely and correctly implement the definition of the program= ming language. (For sufficiently complex programming languages but that bar= is very, very low.*) So Gnat has always been known to have at least one b= ug in it. Yes, it is possible to write provably correct programs in Ada. = (You may want to look at the difference between primitive recursive functio= ns and partial recursive functions in a textbook on theory of computation, = or analysis of algorithms.) The problem is that for some recursive functions, it is not possible to pro= ve that the input to the compiler (in Ada) and the output (in machine langu= age) compute the same function for some partially recursive functions. A co= rollary of this, is that there must be programs for which the compiler outp= ut is incorrect. Otherwise the compiler would constitute an (impossible) p= roof of correctness. Or, the compiler could fail to process some inputs wh= ich is a different type of bug. Why drag all this in here? Ada, and for that matter GNAT come pretty close= to this limit. Applying theorem provers to parts of compilers or to parts= of language definitions can improve the quality of compilers. But anythin= g that requires a language and a compiler for that language to be provably = correct is just not possible. (Actually you can accept a particular compil= er as the definition of the language. That eliminates one source of bugs b= y definition. But along comes G=C3=B6del and some of his inconsistent numb= ers to rain on your party. (G=C3=B6del's proofs rely on a mapping between = partially recursive functions and integers. Some numbers, for any mapping = of PRFs to integers, will result in the (compiled code) stating that the fu= nction has the wrong output. The simplest example is probably the halting = function which cannot be correctly computed. (If anyone ever tells you tha= t there are some things which God did not want man to know, agree and point= to the halting problem. If you don't believe in God, and think that man ca= n know everything, you are still left with the halting problem. ;-)=20 * It may be worth stating that limit here. Regular expressions and finite = state machines are languages beneath the bar. For example, a compiler for = arithmetic expressions can be proven true. Add recursion, and you are over= the line.