To be honest, the system in this paper doesn't really match the Rust system at all. It isn't based on regions and all borrows occur upon function calls, so it's pretty similar to pre-Cyclone alias-tracking features.
For embedded Ada programs, this simpler form is probably sufficient. The main improvement you'd get from Cyclone-style nested regions is being able to type-check functions that produce outputs that are themselves borrowed pointers, either by returning them or storing them in a data structure passed as an argument. In embedded code you're much less likely to have dynamic data structures whose lifetimes are anchored to a given stack frame or control-flow region, so this isn't as useful as it is for the C++11ish coding style encouraged by Rust.
Ada and SPARK predate Rust by decades. For Rust to come on the scene and start influencing them and their well-established community is something that reflects favorably on Rust.
By contrast, when a modern language adopts something from Lisp, that doesn't really say anything new about Lisp. It's been around forever and everyone who actually bothers to learn about the history of programming languages knows Lisp has a lot to teach those who bother to learn. When a new language borrows from Lisp, that says more about the state of the new language author's education than about Lisp itself.
> Ada and SPARK predate Rust by decades. For Rust to come on the scene and start influencing them and their well-established community is something that reflects favorably on Rust.
It definitely does ! And FWIW I work at AdaCore, and even though Rust did not invent those features, I can safely say that the work we do on safe pointer is very directly inspired by Rust.
