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:c0c2:: with SMTP id q185-v6mr11555961iof.134.1528157846116; Mon, 04 Jun 2018 17:17:26 -0700 (PDT) X-Received: by 2002:aca:5208:: with SMTP id g8-v6mr625528oib.1.1528157845893; Mon, 04 Jun 2018 17:17:25 -0700 (PDT) Path: eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!feeder.eternal-september.org!news.uzoreto.com!weretis.net!feeder6.news.weretis.net!feeder.usenetexpress.com!feeder-in1.iad1.usenetexpress.com!border1.nntp.dca1.giganews.com!nntp.giganews.com!v8-v6no347419itc.0!news-out.google.com!f20-v6ni322itd.0!nntp.google.com!v8-v6no347416itc.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail Newsgroups: comp.lang.ada Date: Mon, 4 Jun 2018 17:17:25 -0700 (PDT) In-Reply-To: <878t7u1cfm.fsf@nightsong.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> User-Agent: G2/1.0 MIME-Version: 1.0 Message-ID: Subject: Re: Ada Successor Language From: Shark8 Injection-Date: Tue, 05 Jun 2018 00:17:26 +0000 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Xref: reader02.eternal-september.org comp.lang.ada:52937 Date: 2018-06-04T17:17:25-07:00 List-Id: On Monday, June 4, 2018 at 3:14:57 PM UTC-6, Paul Rubin wrote: > Shark8 writes: > > (1) The Meta language > > (2) The Generic Language > > (3) The Concurrent/Parallelism language > > (4) The Proving language [SPARK] > > (5) The HW/Representation language >=20 > By "Meta language" I first thought you meant replacing the ARM with a > machine checkable specification, written in something like Twelf[1]. > That seems like a great idea. But instead it seems like you want some > general syntactic umbrella in which the other stuff is embedded as > DSL's. I.e. you are reinventing Lisp ;). =20 A little of column-A, a little of column-B. (I would love to get my hands on a copy of the source for Symbolics Ada; it= was awesome to see how integrated it was with the LISP environment -- But = have no Idea where to start for that.) Having the LRM define a nice, relatively-simple, machine-checkable language= which could be used to define everything else would be really, really nice= for compiler developers. Having [some] things formally and explicitly defined in terms of sets would= also be helpful -- see: https://en.wikibooks.org/wiki/Ada_Programming/Type= _System#The_Type_Hierarchy -- having (eg) a real definition of Universal_In= teger would allow some nice definition clean-up. (ALSO: I personally think that a user definable "abstract type interface" [= kinda/sorta type classes], as well as user-definable attributes, would be g= reat ways to handle the above while expanding the capabilities of Ada'Succ.= ) >=20 > Also it's unclear what you mean by the Generic language: is that > supposed to be a special sub-language for type-level programming, > something like ML's module language? I dunno, maybe that should be > closely connected with the proving language. Ada already /has/ a generic language; the whole section on generic formal p= arameters defines it -- https://en.wikibooks.org/wiki/Ada_Programming/Gener= ics#Generic_formal_types -- and these are going to be expanded in Ada 2020,= IIUC, to certain provability properties. >=20 > Concurrency/Parallelism doesn't need a special language: it's mostly > runtime stuff with a bit of compiler backend support and maybe an even > smaller bit of syntactic support. Except it already is its own language TASK, SELECT, and arguably DELAY don'= t really appear in the rest of the language. This is likely going to become more apparent with parallel-blocks and the p= roposed method for mapping. >=20 > The proving language might look quite a bit different from SPARK because > of how much that field has changed since SPARK was new. I wonder if > again a Lisp-inspired approach would be helpful: the language definition > would include a formal spec for AST's that could be handed off to > external proof systems, along with any embedded assertions and contracts > that could be connected up with proofs packaged separately from the user > program. There's some interesting stuff that could be done in this area; for compile= rs we could commandeer the ideas here -- http://citeseerx.ist.psu.edu/viewd= oc/download?doi=3D10.1.1.324.4139&rep=3Drep1&type=3Dpdf and https://pdfs.se= manticscholar.org/d3a1/4b2301487946614ca89ec23726abf27d9f65.pdf and [IIRC t= hese two papers] https://www.cc.gatech.edu/~xzhang36/papers/pldi14b-long.pd= f and http://www.rug.nl/research/portal/files/33882898/Kurs14a_ParsingConte= xt.pdf -- for some really interesting capabilities. >=20 > I wonder if we're in for some big advances in automated proof search any > time soon. I haven't been hearing anything about it but it just seems > like an obvious thing for people to be working on. There were a few papers I read early last year that were interesting, thoug= h I don't remember them off the top of my head.