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