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
Path: 
 eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!.POSTED!not-for-mail
From: Paul Rubin <no.email@nospam.invalid>
Newsgroups: comp.lang.ada
Subject: Re: Ada Successor Language
Date: Mon, 04 Jun 2018 14:14:53 -0700
Organization: A noiseless patient Spider
Message-ID: <878t7u1cfm.fsf@nightsong.com>
References: <5e86db65-84b9-4b5b-9aea-427a658b5ae7@googlegroups.com>
Mime-Version: 1.0
Content-Type: text/plain
Injection-Info: reader02.eternal-september.org;
 posting-host="80a0b3386568bcb6d01d86235f4fbd0e";
	logging-data="2026"; mail-complaints-to="abuse@eternal-september.org";
	posting-account="U2FsdGVkX18pz84xWGlRbwzfM2AIcrEF"
User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/25.3 (gnu/linux)
Cancel-Lock: sha1:ovMPYVgvLAJIqKU9tBb/sG6thBc=
	sha1:A/qesYRKFxYNZfQUKQfCrYf/ckU=
Xref: reader02.eternal-september.org comp.lang.ada:52931
Date: 2018-06-04T14:14:53-07:00
List-Id: <comp.lang.ada>

Shark8 <onewingedshark@gmail.com> 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 ;).  

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.

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.

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.

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.