Re: GNAT GPL is not shareware

[Paul Rubin <no.email@nospam.invalid>]

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.