Re: Ada.Strings.Fixed.Count raises Storage_Error

[rieachus@comcast.net]

On Sunday, June 26, 2016 at 8:51:21 PM UTC-4, Xavier Petit wrote:
 
> Every parameters of a subprogram should be anticipated and produce a 
> coherent behavior. It’s hard but Ada is especially here to make it easier.

Gödel, Escher, Bach: An Eternal Golden Braid, is a 1979 book by Douglas Hofstadter that is now in its 20th edition.

It tries, among other things to explain the reality revealed by Gödel's proofs.  One of those consequences is that you can't build a perfect compiler.  In fact, the gnat in Ada Core Technologies logo is a cute reminder that every compiler must have at least one bug.  Not, these things are so complex they can never be perfect, but even some very simple software tools are subject to Gödel's findings--no system above a rudimentary complexity (embedding of Peano arithmetic) can be bug-free.

Worse, the Halting Problem is a very simple proof that you cannot write a program that will perfectly determine whether a given software program will halt.  (Or not halt, if you work on embedded systems like I did.)

So trying for perfection in compilers, programming languages, and even many software programs is a mug's game.  You can't do it, you don't know where other corner cases are, and you can't even document all of the bugs.  Yes, it is possible to "prove" software correctness for some programs.  But for those same programs, you have just moved the target, from perfect software to perfect requirements.

The Airbus 320 had a major software bug in spite of the correctness proof tools used.  If a plane cross the last waypoint before the destination, the flight guidance system would put the airplane in the correct glidepath for the chosen runway as quickly as possible, even if that location was under a few thousand feet of granite.  Strasbourg suddenly dove straight down.  Oops! Perfect software implementation of a bad requirement. (https://www.flightglobal.com/news/articles/air-france-ceo-jean-cyril-spinetta-defends-rejection-of-gpws-equipment-on-air-inter-a320-fleet-despite-fatal-1992-st-odile-mountainside-crash-210280/ The obfuscation thrown about by Airbus and the French government still continues.  But at least the bug in "flight path angle mode" in the flight controller got fixed.  This list will show you why I still won't fly on an Airbus 310,20, or 21: https://en.wikipedia.org/wiki/Accidents_and_incidents_involving_the_Airbus_A320_family )