3 ms·
Leaks are permitted in rust, and are not a memory safety concern. I don't think that's what he was talking about.
by pitaj 5y ago
Leaks are permitted in rust, and are not a memory safety concern. I don't think that's what he was talking about.
- johnisgood 5y agoI just added that as an extra. The point is that you can have memory safety even if you do free. It may not have been the case with Ada (without SPARK) in the past.
- johnisgood 5y agoI 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.