And rust is unsafe if you use unsafe rust (or even if you use Arc in safe rust and reference count incorrectly).
Ada doesn’t use allocation, remaining 100% memory safe.
Ada doesn’t use allocation, remaining 100% memory safe.
Most of those can be disabled though through the 'restriction' mechanism (look up Pragma Restriction which is very interesting in itself).
SPARK itself can handle and prove some ownership properties but to the best of my knowledge isn't at the level of rust in memory safety on dynamically allocated memory.
It actually is: https://www.adacore.com/uploads/techPapers/Safe-Dynamic-Memo...
And using https://www.adacore.com/sparkpro as a reference (ignore the 'Pro' bit as it's also available in the GPL edition) - anything certified to SPARK Silver level is far safer than any Rust code out there.
I don't believe it's possible to cause unsafety using Arc in safe Rust. I don't know what "reference count incorrectly" means here. Could you explain?