Hacker News Reader

Presumably, if you use formal verification then that includes memory safety anyway? Would seem strange if it does not.

Formal verification requires a spec and a very large, very expensive amount of tooling to be developed.

My understand is that both these things are in work, and that neither of these things exist yet.

Yes, 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.

Reply on news.ycombinator.com