Re: How to get Ada to ?cross the chasm??

["Dan'l Miller" <optikos@verizon.net>]

On Sunday, April 29, 2018 at 4:20:46 PM UTC-5, Paul Rubin wrote:
> gautier_niouzes writes:
> > You definitely missed most of Ada language, because it's standard Ada
> > features.  You can have expressions of types of any complexity
> > returned from a function, as parameters, as operator parameters etc.
> > Catch up!
> 
> Ok, here is I write a nested array in Python:
> 
>    x = [[1, 2], [3, 4], [5,6]]
> 
> In Haskell I can add a type signature (but I don't have to, since the
> compiler can figure it out automatically):
> 
>    x :: [[Integer]]
>    x = [[1, 2], [3, 4], [5,6]]
> 
> Here's a dictionary in Python:
> 
>    { 'alice': 5, 'bob': 10, 'charlie': 15 }
> 
> If there's an equivalent in Ada, that's good to know.
> 
> > Ada has more powerful ways to manage memory, and it's automatic as well.
> > Mostly it's through stack;
> 
> I wouldn't call that more powerful, but it's useful, and compilers for
> gc'd languages sometimes can recognize situations where they can
> stack-allocate stuff.  I do use unique_ptr in C++ so I'm familiar with
> the style.

Paul, if clever typewriting conveniences would be what causes a niche programming language to “cross the chasm”, then Haskell would have crossed the chasm 20 years ago.   What causes a niche programming language to cross the chasm is when people popularly discover en masse that the language practically solves an enormous design problem that is either impractical or annoyingly obtuse to solve in •all• other already-crossed-the-chasm programming languages.  Merely mimicking the syntactic sugar that another already-crossed-the-chasm language already has is not what causes a programming language to cross the chasm (Java notwithstanding, because Java-the-dullard-borrower was pulled forcibly across the chasm due to its very useful frameworks).

For example, of all the already-crossed-the-chasm programming languages (not counting academic-research-only languages), only modern C++{11,14,17} has the ability to write compile-time expressions to manipulate run-time types at compile-time.  It took 3 editions of the standard to fine-tune the beast.  And an ugly-syntaxed beast is certainly is (by torturing parameterized types to be Turing complete)!   And needing language features that in some compilers cause 160-line (!) long error messages to be emitted for source code that at first, second, and third glances sure looks sane and intended.  But C++ can now write libraries (at all or efficiently) that would have been impractical in C++2003 and before.  Hence, C++{11,14,17} has reversed the waning & fading of C++2003, allowing C++{11,14,17} a rare re-crossing of the chasm after C++2003 was slipping back the wrong direction across the chasm.

Randy has a laudable goal of evolving Ada2020 to do something that no other already-crossed-the-chasm language has in its within-the-compiler repertoire:  provably-correct tasking.  It seems to be a race between Randy's vision and Rust's analogous vision, regarding which is first to cross the chasm, Ada2020 or Rust.

In this thread, Randy also touches on evolving Ada itself (not SPARK) to be an automated IV&V to use IEEE's and NASA's term.  (Randy, you should consider embracing IEEE's terminology of verification and validation, jettisoning “validated Ada compiler” for ‘verified* Ada compiler‘ so that then you can put IV&V meat on the conceptual skeleton; Ada needs to prove both of the Vs, not merely one.)  No already-crossed-the-chasm programming language has that degree of provable correctness either.

* To use IEEE's and NASA's terminology, an Ada compiler is •verified• to implement the ARM, but no one except the user community as a whole •validates• that the ARM's prose accomplishes usefulness to the software engineer.  Crossing or not crossing the chasm is a rather good proxy for an overt test of IEEE's & NASA's definition of the validation V.  If the ARG & Ada compiler vendors would have always put as much effort into IEEE's & NASA's validation V as the Ada community puts into the verification V, then Ada would have already crossed the chasm years ago.  Btw, I am not disparaging the ARG, the ARM, Ada2012, or Ada2020; I am merely pointing out that you are ever so close, but thus far lack rigor to move the ARM from tradecraft to mind-clarifying innovative breakthrough.

https://en.wikipedia.org/wiki/Verification_and_validation