From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=unavailable autolearn_force=no version=3.4.4 X-Received: by 2002:a24:1458:: with SMTP id 85-v6mr6316698itg.55.1525098655969; Mon, 30 Apr 2018 07:30:55 -0700 (PDT) X-Received: by 2002:a9d:70d1:: with SMTP id w17-v6mr435491otj.5.1525098655747; Mon, 30 Apr 2018 07:30:55 -0700 (PDT) Path: eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!feeder.eternal-september.org!news.swapon.de!feeder.usenetexpress.com!feeder-in1.iad1.usenetexpress.com!peer03.iad!feed-me.highwinds-media.com!news.highwinds-media.com!f63-v6no2243367itc.0!news-out.google.com!b185-v6ni3671itb.0!nntp.google.com!k65-v6no2242766ita.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail Newsgroups: comp.lang.ada Date: Mon, 30 Apr 2018 07:30:55 -0700 (PDT) In-Reply-To: <87fu3dogk5.fsf@nightsong.com> Complaints-To: groups-abuse@google.com Injection-Info: glegroupsg2000goo.googlegroups.com; posting-host=47.185.233.194; posting-account=zwxLlwoAAAChLBU7oraRzNDnqQYkYbpo NNTP-Posting-Host: 47.185.233.194 References: <1c73f159-eae4-4ae7-a348-03964b007197@googlegroups.com> <87k1su7nag.fsf@nightsong.com> <87po2la2qt.fsf@nightsong.com> <87in8buttb.fsf@jacob-sparre.dk> <87wowqpowu.fsf@nightsong.com> <87efiyuh10.fsf@jacob-sparre.dk> <87vacanebz.fsf@nightsong.com> <87a7tlvppi.fsf@jacob-sparre.dk> <87k1sponey.fsf@nightsong.com> <658b4dfa-6c52-42d0-a289-8c612e6ee6a5@googlegroups.com> <87fu3dogk5.fsf@nightsong.com> User-Agent: G2/1.0 MIME-Version: 1.0 Message-ID: <45b9ca65-a983-4553-a580-d1ccde834c70@googlegroups.com> Subject: Re: How to get Ada to ?cross the chasm?? From: "Dan'l Miller" Injection-Date: Mon, 30 Apr 2018 14:30:55 +0000 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable X-Received-Bytes: 6445 X-Received-Body-CRC: 362619869 Xref: reader02.eternal-september.org comp.lang.ada:51836 Date: 2018-04-30T07:30:55-07:00 List-Id: 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! >=20 > Ok, here is I write a nested array in Python: >=20 > x =3D [[1, 2], [3, 4], [5,6]] >=20 > In Haskell I can add a type signature (but I don't have to, since the > compiler can figure it out automatically): >=20 > x :: [[Integer]] > x =3D [[1, 2], [3, 4], [5,6]] >=20 > Here's a dictionary in Python: >=20 > { 'alice': 5, 'bob': 10, 'charlie': 15 } >=20 > If there's an equivalent in Ada, that's good to know. >=20 > > Ada has more powerful ways to manage memory, and it's automatic as well= . > > Mostly it's through stack; >=20 > 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 progr= amming language to =E2=80=9Ccross the chasm=E2=80=9D, then Haskell would ha= ve crossed the chasm 20 years ago. What causes a niche programming langua= ge to cross the chasm is when people popularly discover en masse that the l= anguage practically solves an enormous design problem that is either imprac= tical or annoyingly obtuse to solve in =E2=80=A2all=E2=80=A2 other already-= crossed-the-chasm programming languages. Merely mimicking the syntactic su= gar that another already-crossed-the-chasm language already has is not what= causes a programming language to cross the chasm (Java notwithstanding, be= cause 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 (no= t 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 beas= t. 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 c= ode 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 be= en impractical in C++2003 and before. Hence, C++{11,14,17} has reversed th= e 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 ch= asm. 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 repertoi= re: provably-correct tasking. It seems to be a race between Randy's visio= n 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 consi= der embracing IEEE's terminology of verification and validation, jettisonin= g =E2=80=9Cvalidated Ada compiler=E2=80=9D for =E2=80=98verified* Ada compi= ler=E2=80=98 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-th= e-chasm programming language has that degree of provable correctness either= . * To use IEEE's and NASA's terminology, an Ada compiler is =E2=80=A2verifie= d=E2=80=A2 to implement the ARM, but no one except the user community as a = whole =E2=80=A2validates=E2=80=A2 that the ARM's prose accomplishes usefuln= ess to the software engineer. Crossing or not crossing the chasm is a rath= er good proxy for an overt test of IEEE's & NASA's definition of the valida= tion V. If the ARG & Ada compiler vendors would have always put as much ef= fort into IEEE's & NASA's validation V as the Ada community puts into the v= erification V, then Ada would have already crossed the chasm years ago. Bt= w, 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 th= e ARM from tradecraft to mind-clarifying innovative breakthrough. https://en.wikipedia.org/wiki/Verification_and_validation