I think it's supposed to be safe in Ada by default? As far as I can tell, basic allocated objects cannot be deallocated without an "unchecked" operation, and ac

I think it's supposed to be safe in Ada by default? As far as I can tell, basic allocated objects cannot be deallocated without an "unchecked" operation, and access objects created from "aliased" declarations are subject to scoping rules [0]. (If you want to know the full details, go figure out however "accessibility levels" are supposed to work [1].) It should preclude functions from returning access objects without a "prefix'Unchecked_Access" operation. I'm not sure how SPARK's borrowing system is tied into all of this. [0] https://www.adaic.org/resources/add_content/docs/craft/html/ch11.htm https://www.adaic.org/resources/add_content/docs/craft/html/... [1] http://www.ada-auth.org/standards/22rm/html/RM-3-10-2.html http://www.ada-auth.org/standards/22rm/html/RM-3-10-2.html