http://www.electronicdesign.com/embedded-revolution/assessin...
This Barnes book shows how it’s systematically designed for safety at every level:
https://www.adacore.com/books/safe-and-secure-software
Note: The AdaCore website has a section called Gems that gives tips on a lot of useful ways to apply Ada.
Finally, if you do Ada, you get the option of using Design-by-Contract (built-in to 2012) and/or SPARK language. One gives you clear specifications of program behavior that take you right to source of errors when fuzzing or something. The other is a smaller variant of Ada that integrates into automated, theorem provers to try to prove your code free of common errors in all cases versus just ones you think of like with testing. Those errors include things like integer overflow or divide by zero. Here’s some resources on those:
http://www.eiffel.com/developers/design_by_contract_in_detai...
https://en.wikipedia.org/wiki/SPARK_(programming_language)
https://www.amazon.com/Building-High-Integrity-Applications-...
The book and even language was designed for people without a background in formal methods. I’ve gotten positive feedback from a few people on it. Also, I encouraged some people to try SPARK for safer, native methods in languages such as Go. It’s kludgier than things like Rust designed for that in mind but still works.
GPL download for AdaCore GNAT: