Hacker News new | ask | show | jobs
by Filligree 52 days ago
Presumably, if you use formal verification then that includes memory safety anyway? Would seem strange if it does not.
1 comments
irishcoffee 52 days ago
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.

link
eggy 52 days ago
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.
link
irishcoffee 52 days ago
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.

link