I would also like to add these: > Values of such an access type can be deallocated safely. GNATprove generates verification conditions to ensure that no memory

I would also like to add these: > Values of such an access type can be deallocated safely. GNATprove generates verification conditions to ensure that no memory can be leaked. So... you can deallocate safely AND verify that no memory is leaked. Is it not wonderful? - https://docs.adacore.com/live/wave/spark2014/html/spark2014_ug/en/source/access.html#pointer-support-and-dynamic-memory-management https://docs.adacore.com/live/wave/spark2014/html/spark2014_... - https://docs.adacore.com/live/wave/spark2014/html/spark2014_ug/en/usage_scenarios.html#prove-absence-of-run-time-errors-aorte https://docs.adacore.com/live/wave/spark2014/html/spark2014_... > SPARK builds on the strengths of Ada to provide even more guarantees statically rather than dynamically. As summarized in the following table, Ada provides strict syntax and strong typing at compile time plus dynamic checking of run-time errors and program contracts. SPARK allows such checking to be performed statically. In addition, it enforces the use of a safer language subset and detects data flow errors statically.