I spent a lot of time circa 2009/2010 teaching myself Ada for similar reasons. I work in avionics systems (or used to, present job is not) and Ada is grossly underutilized. I’d be willing to wager half the bugs that I saw make it to the testers or, worse, the field would not have happened if we’d used Ada (and used the type system properly).

And these days, using Spark, even more bugs could be detected before compilation even succeeds. But no one wanted to use it at any of my jobs, and that knowledge has mostly atrophied from disuse.

Using Spark contracts to specify and verify low level requirements should be a huge time saver. I too don't understand why everybody seems to use C/C++ nowadays. I guess commercial Ada is just too expensive.

Here's a 1/2 hour webcast on the interaction of programming language and software lifecycle costs. Not too old. https://www.vdcresearch.com/_documents/briefs/IoT/18-Control...

Here's extensive research results based on function point analysis. http://www.ifpug.org/wp-content/uploads/2017/04/IYSM.-Thirty...

Whole lotta' mything going on!

There is a group trying to bring contracts to C++, and Spark is something they have looked at for guidance. I'm not sure of the progress, last I checked there were conflicts on how to use them. That is the compiler guys wanted to use the contract to optimize farther, while the safety guys said that is insane: you don't know if the contract is proved.

They are starting to:

https://www.adacore.com/press/adacore-enhances-security-crit...

https://www.adacore.com/press/iso-26262

https://www.adacore.com/press/jtekt-spark-pro-automotive

https://www.adacore.com/press/denso-spark-automotive-researc...

https://www.adacore.com/press/adacore-tools-streamline-devel...