Suppose you could have memory safety in C by implementing a borrow checker for every individual function. It would be suitable for certain industries, but breat

Suppose you could have memory safety in C by implementing a borrow checker for every individual function. It would be suitable for certain industries, but breathtakingly expensive, error-prone, and therefore useless for most kinds of software. That's roughly the situation today with SPARK. Using Ada does not automatically buy you memory safety on the same level as Rust. You can get a lot further with SPARK, but the annotations are very cumbersome to write. These are well-known problems in the Ada community. There are efforts underway to improve SPARK's ergonomics by adapting ideas from Rust, with the help of the Rust Foundation. Someday soon, Ada will be much closer to Rust's sweet spot on the safety/productivity graph. In the meantime, there are CVEs to patch.