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

[Robert Eachus <rieachus@comcast.net>]

On Tuesday, November 21, 2017 at 8:19:28 PM UTC-5, Randy Brukardt wrote:
 
> 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).

I'm going to be the grinch here and invite Gödel to the party. The name 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 programming language. (For sufficiently complex programming languages but that bar is very, very low.*)  So Gnat has always been known to have at least one bug in it.  Yes, it is possible to write provably correct programs in Ada.  (You may want to look at the difference between primitive recursive functions 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 prove that the input to the compiler (in Ada) and the output (in machine language) compute the same function for some partially recursive functions. A corollary of this, is that there must be programs for which the compiler output is incorrect.  Otherwise the compiler would constitute an (impossible) proof of correctness.  Or, the compiler could fail to process some inputs which 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 anything that requires a language and a compiler for that language to be provably correct is just not possible.  (Actually you can accept a particular compiler as the definition of the language.  That eliminates one source of bugs by definition.  But along comes Gödel and some of his inconsistent numbers to rain on your party.  (Gödel'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 function has the wrong output.  The simplest example is probably the halting function which cannot be correctly computed.  (If anyone ever tells you that 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 can know everything, you are still left with the halting problem. ;-) 

* 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.