Thank you! I assume 'Access types are not memory-safe, right? Is there a SPARK equivalent which still does not copy (i.e. it only references) that is memory safe?
To be more specific, how would one implement something like a "Get_First_Word" or "Trim_Whitespace" without copying?
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.
To be more specific, how would one implement something like a "Get_First_Word" or "Trim_Whitespace" without copying?