Re: Ada.Strings.Fixed.Count raises Storage_Error

[rieachus@comcast.net]

On Wednesday, June 29, 2016 at 3:57:47 PM UTC-4, Dmitry A. Kazakov wrote:

> Goedel results don't apply to programs anyway, because you are not 
> required to decide anything using the program at hand. You are free to 
> use *another* program, so you can break out.

Sigh! Gödel proved not just that there are systems where some functions cannot be computed correctly, but that there are functions which cannot be computed correctly by any system.  There are systems which are not powerful enough to try to compute these functions, but those systems are very limited.  Regular expressions are an example of such a limited system, Ada compilers are not.
 
> Nor the Halting problem does apply. For any program having a finite 
> number of states, one clearly can decide in finite time with finite 
> storage whether the program halts.

Since when have Ada compilers dealt with only finite states?*  There are programming languages which do have such limits, but Fortran, PL/I, Ada, C++, and other general purpose programming languages are not among them.  It is nice to think you live inside a little box, but Ada compilers can (and do) deal with programs in chunks called compilation units, and programs can be extended over multiple physical processors, each of which can accept external files as input.

To be explicit, theorem proving systems are attempts to solve the halting problem.  You hope that your theorem prover will give a correct answer or give up, but the reality is that there are programs that are never handed to theorem provers because they will execute "forever" without finding an answer.

Ada 80 had a statement that compilers were expected to find a valid elaboration order, and if one did not exist, the program was illegal.  So I, tongue in cheek, wrote a program which was legal if--and only if--Format's Last Theorem was false.  Oops!  Rules were changed so that compilers can leave those edge cases until run-time, and for most programs compilers will find an elaboration order which does not need to check for elaboration errors.  (So now you can compile that program, and a theorem prover that can handle FLT can prove that it never halts, or maybe prove that it halts when your bignum package runs out of file storage. ;-)

* You may contend that your personal computer has a finite number of states, but well before you can finish enumerating them, you will upgrade the processor, memory, and/or disks (whether mechanical or solid state).  And then there are services like Drop Box which enable you to store data "in the cloud."  So the time when computers had a finite set of states is long past.  (Even Univac I, with 1000 words of memory, had ten tape drives, and an operator to mount new tapes when required.)