alt Hacker NewsFormal 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.
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.