[FabienC]

The focus of Ada is not on safe arithmetic only, it's on functional safety at large: the code does what it is specified to do and nothing else.

Ada shines in its specification power, how developers can express what the code is supposed to do (strong typing, ranges, contracts, invariants, generics, etc.). And then you can either check your code at "compile time" with SPARK [1], that provides a mathematical proof that you code follows the specification. SPARK also proves that you don't have buffer overflows or division by zero for instance. Or you can have checks inserted in the run-time code which greatly improves the benefits of testing as every deviation from specifications will be detected, not only the ones you decided to check in your tests.

In terms of memory safety, Ada always had an edge on C/C++ because of the lower usage of pointers (see parameter modes [2]) and the emphasis on stack allocation. Now with the introduction of ownership in SPARK it's getting on par with Rust on that topic.

[1] https://learn.adacore.com/courses/intro-to-spark/chapters/05... [2] https://learn.adacore.com/courses/intro-to-ada/chapters/subp...

[quotemstr]

Interesting. I wasn't aware that safety in Ada had developed to this point. Maybe I'll have to take another look at the language!