alt Hacker NewsYes, and AdaCore's tooling is formally verified and produces reports already familiar to aerospace, railway, and auto auditors for verifying certifications making it attractive to this industry segment of high-integrity apps. Memory safety is taken care of mainly through the features Ada/SPARK2014 offer in creating safe, high-integrity programs, correct.
Yeah right now it’s usually C, but if I had a choice I’d use Ada. I’ve never done a graphical interface with Ada, and I have with OpenGLSC using C.
I’m sure at some point there will be an accepted formal verification toolchain for rust, I hope to never use it.