5 ms·

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% mem

by 3a2d29 4y ago

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.

pornel 4y ago
Arc in safe Rust won't let you cause use-after-free no matter how much you screw up.
twic 4y ago
> And rust is unsafe if you use unsafe rust (or even if you use Arc in safe rust and reference count incorrectly). 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?
- vitiral 4y ago
  I believe they are referring to memory leaks. Not really a "safety concern" as it will simply cause the application to crash (eventually).
touisteur 4y ago
Erm it is perfectly possible to perform dynamic allocation in Ada. You have the 'new' keyword to allocate a new object of a type. You have the 'unchecked deallocation' mechanism. You have controlled types that deallocate when an object is out of scope. You have all sorts of weak references schemes in some libraries. You have storage pools to handle allocation specifics for a type. You have the secondary stack that handles returning objects of unknown-size-at-call-site. 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.
- topdancing 4y ago
  > 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-Memory-Management-in-Ada-and-SPARK.pdf https://www.adacore.com/uploads/techPapers/Safe-Dynamic-Memo... And using https://www.adacore.com/sparkpro 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.
  - touisteur 4y ago
    Seems I missed some of the progress... Things are moving fast these days.

by 3a2d29 4y ago

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.

pornel 4y ago

Arc in safe Rust won't let you cause use-after-free no matter how much you screw up.

twic 4y ago

> And rust is unsafe if you use unsafe rust (or even if you use Arc in safe rust and reference count incorrectly). 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?

vitiral 4y ago
I believe they are referring to memory leaks. Not really a "safety concern" as it will simply cause the application to crash (eventually).

touisteur 4y ago

Erm it is perfectly possible to perform dynamic allocation in Ada. You have the 'new' keyword to allocate a new object of a type. You have the 'unchecked deallocation' mechanism. You have controlled types that deallocate when an object is out of scope. You have all sorts of weak references schemes in some libraries. You have storage pools to handle allocation specifics for a type. You have the secondary stack that handles returning objects of unknown-size-at-call-site. 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.

topdancing 4y ago
> 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-Memory-Management-in-Ada-and-SPARK.pdf https://www.adacore.com/uploads/techPapers/Safe-Dynamic-Memo... And using https://www.adacore.com/sparkpro 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.
- touisteur 4y ago
  Seems I missed some of the progress... Things are moving fast these days.