[0815test]

I don't think Ada has anything like the Rust borrow-checker! A feature-set comparable to SPARK will need to wait until a better characterization of Rust Unsafe code is achieved, but in the long term it is absolutely a goal to be able to write Rust code that carries "contracts" for its use of unsafe features, and/or "proofs" that the code meets some specification.

[pjmlp]

Actually SPARK is going to have an ownership model as well.

https://fosdem.org/2019/schedule/event/ada_pointers/