2 ms·
Although temporarily displaced by Rust, this additions means Ada+SPARK is back to being the safest solution for system programming. The only thing it's lacking
by nickpsecurity 8y ago
Although temporarily displaced by Rust, this additions means Ada+SPARK is back to being the safest solution for system programming. The only thing it's lacking is a certifying compiler or translation validation. Compiler errors can invalidate the safety of the language. Safe subsets of C have it beat there with stuff like C0, CompCert, and KCC. There's even memory-safe variants of x86 assembly. Fortunately, there is ongoing work on the source-to-assembly verification of SPARK programs.