A policy statement on open-source software from the White House

Posted Mar 14, 2016 17:34 UTC (Mon) by zmower (subscriber, #3005)
In reply to: A policy statement on open-source software from the White House by eru
Parent article: A policy statement on open-source software from the White House

And railway systems, air traffic control, medical devices and defence. I still write Ada (professionally and hobby). My contribution to mal (make-a-lisp) is incoming.

A policy statement on open-source software from the White House

Posted Mar 14, 2016 23:02 UTC (Mon) by apoelstra (subscriber, #75205) [Link] (2 responses)

Have any Ada folks looked seriously at Rust? Does it hold promise to be an Ada replacement?

A policy statement on open-source software from the White House

Posted Mar 14, 2016 23:09 UTC (Mon) by Cyberax (✭ supporter ✭, #52523) [Link] (1 responses)

It's much better than Ada at actual typechecks and verification.

Ada is somewhat fetishized in this regard, but in reality it's not really better than other languages.

A policy statement on open-source software from the White House

Posted Mar 18, 2016 7:59 UTC (Fri) by dvdeug (guest, #10998) [Link]

Compared to C, it has actual type declarations, not just typedefs. Enums are actually enums, not integers. There are numeric subtypes of detail I've not seen in any other language. It may be a Pascal descendant, and not a functional programming language with fancy typing, but it's a lot better than its statically compiled competitors, with the possible exception of Rust and several other new and infrequently used languages.

The most recent version, Ada 2012, has container libraries where the size is statically set so the amount of memory the program uses can be rigorously controlled without giving up the use of a powerful container library. That too, as far as I know, is unique to Ada, probably because worrying about memory is a bit of niche market.

As far as I know, SPARK, an Ada subset, is the only statically compiled formally proven language available as open source. There's also Coq and friends, but the market for a statically verified Haskell dialect is a bit different from the market for an Ada subset with the power of Modula-2.

There are statically verified C subsets, but not open source, as far as I know.