Safe Dynamic Memory Management in Ada and SPARK

Ada as a language is super cool. It's tasking model is neat, and was built into the language in 1995. You can use arbitrary Enums to index arrays, it has bounded numerical types, it's just a neat language.

Ada's main drawbacks, aren't Ada's. It's that the US Army pushed it so hard, it's terminally "uncool." Also many people and organizations that use it are defense contractors, so being half-decent at Ada is seen as a "competitive advantage." This makes learning Ada a challenge. It's good to see that there are some more resources for learning Ada! I really wish that the learn.adacore.com was up a few years ago. I could have used it.

Although temporarily displaced by Rust, this additions means Ada+SPARK is back to being the safest solution for system programming. The only thing it's lacking is a certifying compiler or translation validation. Compiler errors can invalidate the safety of the language. Safe subsets of C have it beat there with stuff like C0, CompCert, and KCC. There's even memory-safe variants of x86 assembly. Fortunately, there is ongoing work on the source-to-assembly verification of SPARK programs.

For those who want to try SPARK, we just launched an interactive learning website: https://learn.adacore.com