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

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.