Re: Ada Successor Language

[Shark8 <onewingedshark@gmail.com>]

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
> 
> 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 ;).  

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_Integer 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 great ways to handle the above while expanding the capabilities of Ada'Succ.)

> 
> 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 parameters defines it -- https://en.wikibooks.org/wiki/Ada_Programming/Generics#Generic_formal_types -- and these are going to be expanded in Ada 2020, IIUC, to certain provability properties.

> 
> 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 proposed method for mapping.

> 
> 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 compilers we could commandeer the ideas here -- http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.324.4139&rep=rep1&type=pdf and https://pdfs.semanticscholar.org/d3a1/4b2301487946614ca89ec23726abf27d9f65.pdf and [IIRC these two papers] https://www.cc.gatech.edu/~xzhang36/papers/pldi14b-long.pdf and http://www.rug.nl/research/portal/files/33882898/Kurs14a_ParsingContext.pdf -- for some really interesting capabilities.

> 
> 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, though I don't remember them off the top of my head.