3 ms·
In the space of safety-critical software systems with tight constraints, Ada has typically been the go-to language. Together with the verification sub-language,
by yawaramin 8y ago
In the space of safety-critical software systems with tight constraints, Ada has typically been the go-to language. Together with the verification sub-language, SPARK, it can prove things like array bounds (and I assume integer bounds) are respected, without runtime checks. See e.g. https://www.adacore.com/gems/gem-68 https://www.adacore.com/gems/gem-68
The formal verification method used by SPARK is industry-proven (for decades). Dependent types are for the most part still an academic curiosity struggling to find industrial application. Of course they may very well do that, one day. But today, if you're working on safety-critical systems, I hope you take a close look at Ada+SPARK.