by Quentin Ochem – Oct 07, 2024. At AdaCore, we’re in the business of supporting people who develop high-integrity software, in particular for embedded systems. In terms of programming languages, this means supporting the most commonly found candidates, which in 2024 include C/C++, Ada/SPARK, and…
agreed, and you have to get the proofs perfect, in whatever language in which they are expressed, to be useful. like you have to get the code correct twice to make sure it works once.
i think having safe patterns/apis where the compiler can automatically spot classes of potential error is a better approach