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: How to get Ada to ?cross the chasm??
Date: Tue, 01 May 2018 19:07:17 -0700
Organization: A noiseless patient Spider
Message-ID: <87bmdyolnu.fsf@nightsong.com>
References: <1c73f159-eae4-4ae7-a348-03964b007197@googlegroups.com>
	<dbcb51b9-8ab9-4d39-bb70-47fdb15ebfd8@googlegroups.com>
	<pb7eii$bf1$1@dont-email.me>
	<b75ad71f-a917-4638-9b38-ccfe69b04e53@googlegroups.com>
	<slrnpdpiv9.ntv.address@is.invalid>
	<pbr3mi$leu$1@franka.jacob-sparre.dk> <87k1su7nag.fsf@nightsong.com>
	<pbtlno$3k2$1@franka.jacob-sparre.dk> <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>
	<45b9ca65-a983-4553-a580-d1ccde834c70@googlegroups.com>
Mime-Version: 1.0
Content-Type: text/plain; charset=utf-8
Content-Transfer-Encoding: 8bit
Injection-Info: reader02.eternal-september.org;
 posting-host="c542ccd1be7cc45dffb8a8de81e34fd0";
	logging-data="16313"; mail-complaints-to="abuse@eternal-september.org";
	posting-account="U2FsdGVkX1+UdsRZvP8zGteDwwe1LyTV"
User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/25.3 (gnu/linux)
Cancel-Lock: sha1:affus+vsBe08qJHzy/XSxn3SJtA=
	sha1:+Cop1kHLdn6Sm2AwkGWvH87aQNk=
Xref: reader02.eternal-september.org comp.lang.ada:51907
Date: 2018-05-01T19:07:17-07:00
List-Id: <comp.lang.ada>

"Dan'l Miller" <optikos@verizon.net> writes:
> For example, of all the already-crossed-the-chasm programming
> languages (not 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.

I don't understand what you mean by that: something like Haskell GADT's
(Ocaml has them too)?  It's certainly possible to have them without
making the type system Turing-complete.  C++ template metaprogramming is
Turing complete by complete accident, with the implementers surprised
when someone showed how to write a template that generated an error
message containing a list of prime numbers computed in the template
expansion ;-).

Here's an interesting challenge about statically validated API's using
types.  It's pretty straightforward in Haskell, and ugly solutions exist
in C++ and Java.  It's almost certainly impossible in C.  I've been
wondering whether Ada can do it and I've been wanting to read up on
Ada's type system to find out.  I wouldn't hold it against Ada if it
can't though, since Ada makes a reasonable choice in offloading complex
verification conditions to provers like SPARK:

http://blog.tmorris.net/posts/understanding-practical-api-design-static-typing-and-functional-programming/

> * To use IEEE's and NASA's terminology, an Ada compiler is •verified•

I wouldn't use that term any more.  In high-assurance programming
verified means mechanically checked with a proof system.

I'm looking forward to Ada2020 and it will be great if Randy implements
it.