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=unavailable autolearn_force=no version=3.4.4 Path: eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!feeder.eternal-september.org!gandalf.srv.welterde.de!news.jacob-sparre.dk!franka.jacob-sparre.dk!pnx.dk!.POSTED.rrsoftware.com!not-for-mail From: "Randy Brukardt" Newsgroups: comp.lang.ada Subject: Re: More reliable compilers (of some programming langauges) than GNAT Date: Tue, 21 Nov 2017 19:19:27 -0600 Organization: JSA Research & Innovation Message-ID: References: <2fca0f38-833e-485d-9a38-febcdd507bb1@googlegroups.com> Injection-Date: Wed, 22 Nov 2017 01:19:27 -0000 (UTC) Injection-Info: franka.jacob-sparre.dk; posting-host="rrsoftware.com:24.196.82.226"; logging-data="19158"; mail-complaints-to="news@jacob-sparre.dk" X-Priority: 3 X-MSMail-Priority: Normal X-Newsreader: Microsoft Outlook Express 6.00.2900.5931 X-RFC2646: Format=Flowed; Original X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2900.7246 Xref: feeder.eternal-september.org comp.lang.ada:49046 Date: 2017-11-21T19:19:27-06:00 List-Id: "AdaMagica" wrote in message news:2fca0f38-833e-485d-9a38-febcdd507bb1@googlegroups.com... > Am Dienstag, 21. November 2017 16:07:47 UTC+1 schrieb Victor Porton: ... >> Would you recommend me another language (not Ada) which has a quality >> free >> compiler? > > compilers free of quality should be abundant for languages galore. LoL. I think the smily face is missing here. :-) Seriously, though, the idea of a bug-free compiler for any non-trivial programming language is rather laughable. It's possible that the application of proof tools to compilers will improve their quality (especially possible in the back-ends), but there is always going to be the problem of adequately expressing the correct result. One would have to have a completely formal description of the programming language -- but then how would one prove that there are no bugs in that formal description (most likely written in a language that hardly anyone would understand)? You have a problem that essentially is an infinite regress - you're always going to end up at some point with a description that cannot be proved correct (and is too complex to ensure correct). (Note: There was a formal description and set of proofs for part of the Ada 95 definition; supposedly, it proved that there was no problems with the visibility description of Ada 95; in particular that there were no Beaujolais effects. But no one other than the authors understood it and nothing further was ever done with it so far as I know.) Randy.