Re: More reliable compilers (of some programming langauges) than GNAT

["Randy Brukardt" <randy@rrsoftware.com>]

"AdaMagica" <christ-usch.grein@t-online.de> 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.