Ada was not designed for formal verification. It was designed to build safety-critical software and to standardize and unify the US Department of Defense's pan

Ada was not designed for formal verification. It was designed to build safety-critical software and to standardize and unify the US Department of Defense's panoply of programming languages. "SPARK is a programming language and a set of verification tools designed to meet the needs of high-assurance software development. SPARK is based on Ada, both subsetting the language to remove features that defy verification and also extending the system of contracts by defining new Ada aspects to support modular, constructive, formal verification." Source: https://docs.adacore.com/spark2014-docs/html/lrm/introduction.html https://docs.adacore.com/spark2014-docs/html/lrm/introductio... >> Both dynamics are bringing Ada adoption to a stop. It may be a shame but that’s what I see. I disagree. The success of Rust as a replacement for C++ has brought a renewed interest to Ada. Rust has many great ideas and many of them are being added to SPARK. Several ideas from Ada will likely be added to Rust as work from Ferrous Systems and others prepares Rust for use in safety-critical domains.