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=-0.9 required=5.0 tests=BAYES_00,FORGED_GMAIL_RCVD, FREEMAIL_FROM autolearn=no autolearn_force=no version=3.4.4 X-Received: by 2002:a6b:a207:: with SMTP id l7-v6mr1196308ioe.134.1528479204339; Fri, 08 Jun 2018 10:33:24 -0700 (PDT) X-Received: by 2002:aca:d5d0:: with SMTP id m199-v6mr252103oig.9.1528479204188; Fri, 08 Jun 2018 10:33:24 -0700 (PDT) Path: eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!feeder.eternal-september.org!news.linkpendium.com!news.linkpendium.com!news.snarked.org!border2.nntp.dca1.giganews.com!nntp.giganews.com!v8-v6no1000351itc.0!news-out.google.com!c20-v6ni320itc.0!nntp.google.com!v8-v6no1000349itc.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail Newsgroups: comp.lang.ada Date: Fri, 8 Jun 2018 10:33:23 -0700 (PDT) In-Reply-To: <8a65f8ff-4a75-43f2-884c-6872780f7ea8@googlegroups.com> Complaints-To: groups-abuse@google.com Injection-Info: glegroupsg2000goo.googlegroups.com; posting-host=76.113.16.86; posting-account=lJ3JNwoAAAAQfH3VV9vttJLkThaxtTfC NNTP-Posting-Host: 76.113.16.86 References: <5e86db65-84b9-4b5b-9aea-427a658b5ae7@googlegroups.com> <878t7u1cfm.fsf@nightsong.com> <8a65f8ff-4a75-43f2-884c-6872780f7ea8@googlegroups.com> User-Agent: G2/1.0 MIME-Version: 1.0 Message-ID: <771e8e35-b71a-499d-a0fe-bb0df1de22ab@googlegroups.com> Subject: Re: Ada Successor Language From: Shark8 Injection-Date: Fri, 08 Jun 2018 17:33:24 +0000 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Xref: reader02.eternal-september.org comp.lang.ada:53005 Date: 2018-06-08T10:33:23-07:00 List-Id: On Friday, June 8, 2018 at 10:28:04 AM UTC-6, Dan'l Miller wrote: > > This formalization will not be easy or cheap, > > but should be feasible today, at least for the > > syntax and static semantics.=20 >=20 > Who would be willing to fund such an effort? Perhaps this is the wrong question. The big problem being so few with resou= rces have bought into Ada -- and those that have (eg Boeing) seem to either= be transitioning away, or satisfied with state of things and uninterested = in improvement. I have a few contacts locally who might be interested, given the proper pre= sentation; I'm trying to write up a proposal about it. / I could probably u= se some help doing so, but I plan to present it first and foremost as a ful= l-IDE (and fully verified) for HW and SW. (pop me an e-mail if you're inter= ested in helping.) > 1) fizzle: The big tech companies on the West Coast of the USA seem highl= y disinterested in safety. While I agree based on my experiences, and attitudes in lower management co= rporately; do you have any citable references on this? It would help boost = my proposal, I think. > 2) fizzle: DARPA seems to have moved on to AI & robotics only, not all th= e goals that motivated Ada. Sad, and stupid. -- "AI" as it is now is nothing less than pattern-matching= and while necessary for AI is not sufficient. (For true AI, we're about at= the level of "epileptic chicken".)=20 > 3) fizzle: INRIA seems more interested in OCaml than Ada. Well, given the hype-wave of "functional programming" this is at least unde= rstandable. Though, IIRC, there were some fans/proponents of Ada there. > 3) potential: The most likely funding would come from national government= s in Europe, especially France or Germany, who are at times pursuing safe s= oftware systems. Interesting. > What allied hot topic would attract funding to translating the _LRM_ into= some sort of formal-specifications language? Ada as required by the insur= ance industry? Ada for robotics? AI for Ada? Ada for blockchain currency= ? Honestly, I think Ada at the systems-level would work well. Microsoft Resea= rch did a fully type-safe OS (Verve) a while back and the researchers were = blown away by the lack of need for a debugger: https://www.microsoft.com/en= -us/research/wp-content/uploads/2016/02/pldi117-yang.pdf -- You can almost = hear the amazement off those paragraphs.