I don't know them well enough to compare. Haven't been coding in a while. Best resource on Ada to do that comparison is Barnes: https://www.adacore.com/books/s

I don't know them well enough to compare. Haven't been coding in a while. Best resource on Ada to do that comparison is Barnes: https://www.adacore.com/books/safe-and-secure-software https://www.adacore.com/books/safe-and-secure-software SPARK is a subset without pointers that feeds information about the program into solvers that prove absence of common classes of errors like overflows and divide by zero. Inspired by Rust, recent work is adding pointers. Praxis' Correct-by-Construction defaulted on Ada with SPARK saved for most critical stuff, esp safety- or security-enforcing. Right now, Rust is mainly ahead of Ada on dealing with the pointer safety and better safe concurrency. Ada's Ravenscar aimed for safety but was restrictive. That's my take.