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!news.eternal-september.org!mx02.eternal-september.org!.POSTED!not-for-mail
From: Paul Rubin <no.email@nospam.invalid>
Newsgroups: comp.lang.ada
Subject: Re: GNAT GPL is not shareware
Date: Thu, 08 Jan 2015 22:50:54 -0800
Organization: A noiseless patient Spider
Message-ID: <874ms0tpkh.fsf@jester.gateway.sonic.net>
References: <87bnmetex4.fsf@ludovic-brenta.org>
	<87lhlirpk0.fsf@ludovic-brenta.org>
	<bb6afd60-da67-4b0a-93ca-2921b985cc3e@googlegroups.com>
	<m8ds96$po2$1@news.albasani.net>
	<79f3eff7-2b45-40ae-af94-fa9a17426d82@googlegroups.com>
	<87bnmd8mg2.fsf@ixod.org>
	<19cf9bc2-f8b9-4735-b427-7b070dda59da@googlegroups.com>
	<qfbmaal82onf3ho5otthp0m6vbraaavoq5@4ax.com>
	<ohGqw.195991$rq4.58661@fx27.iad>
	<fa17b731-a99f-4d51-b7e9-806bb2de00c6@googlegroups.com>
	<s7Jqw.1026393$Lj7.973937@fx22.iad>
	<alpine.DEB.2.11.1501061414310.19142@debian>
	<m8gsds$klt$1@dont-email.me>
	<72ede803-e2e9-4e21-a415-457374bef87d@googlegroups.com>
	<m8hfmq$u9e$1@loke.gir.dk>
	<1337ca4c-a19e-468e-bc07-5412438f662b@googlegroups.com>
	<m8kfu7$mu6$1@loke.gir.dk>
	<17ad25fe-e04f-4d79-a622-0b2455c150a0@googlegroups.com>
	<m8nd0g$r7g$1@loke.gir.dk> <87sifku151.fsf@jester.gateway.sonic.net>
	<0e193630-51f8-4a9b-a3f3-9a696ab7f995@googlegroups.com>
Mime-Version: 1.0
Content-Type: text/plain
Injection-Info: mx02.eternal-september.org;
 posting-host="9be1734e45595b2e29ecbdd3ce926380";
	logging-data="13336"; mail-complaints-to="abuse@eternal-september.org";
	posting-account="U2FsdGVkX18Msh3tw1hh4fuiCZuEONCc"
User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/24.3 (gnu/linux)
Cancel-Lock: sha1:owQ2qz824IUrift03FdpNNvWQPE=
	sha1:eZ0n4HAyyHZEDCdnVkLVdyhDdwg=
Xref: news.eternal-september.org comp.lang.ada:24497
Date: 2015-01-08T22:50:54-08:00
List-Id: <comp.lang.ada>

David Botton <david@botton.com> writes:
>> Give ____ a try, http://_ohnoyoudon't.org_ .
> Begone troll! Off with ye head!

Heh, I'm not trying to troll, Ada is just designed to work in the
intersection of a bunch of different niches (highly correct code,
realtime code, code that runs in constrained environments) and that's
why there's not that many programmers involved in it.  If you're mostly
interested in writing solid, correct code but can look outside the
embedded and realtime niches, there's plenty going on.  

Take a look at http://compcert.inria.fr which is about a formally
verified C compiler (who knows, maybe it might compile Ada sometime too)
written in Coq generating Ocaml.  Ada isn't really the right vehicle for
it since it's not realtime and it runs on big computers, so it can use
garbage collection and simpler verification techniques than Ada uses.
But it's IMHO still of extreme interest to people wanting to write code
with high-end correctness assurance.  The ohnoyoudon't link I gave can
be seen as a stepping-stone to those methods.