The article fails to mention Ada's capabilities in the area of formal verification. The 'SPARK' subset of the language is designed explicitly for this purpose.

The article fails to mention Ada's capabilities in the area of formal verification. The 'SPARK' subset of the language is designed explicitly for this purpose. Modern Ada/SPARK also support Rust style 'safe-pointers': https://blog.adacore.com/using-pointers-in-spark https://blog.adacore.com/using-pointers-in-spark