4 ms·

No, Ada has no lifetimes and borrow checking and thus cannot possibly offer the same expressiveness as Rust while supporting safe memory deallocation without ga

by devit 5y ago

No, Ada has no lifetimes and borrow checking and thus cannot possibly offer the same expressiveness as Rust while supporting safe memory deallocation without garbage collection.

pjmlp 5y ago
That is why SPARK exists, and RAII offers safe memory deallocation. Ada never used GC, although Ada 83 allowed for optional implementation, that no compiler ever made use of, thus it was removed from Ada standard in the 2005 revision.
johnisgood 5y ago
You may want to read https://www.adacore.com/uploads/techPapers/Safe-Dynamic-Memory-Management-in-Ada-and-SPARK.pdf https://www.adacore.com/uploads/techPapers/Safe-Dynamic-Memo.... It talks plenty about lifetimes and borrowing. It even mentions Rust (and ParaSail). > The goal is to allow a pattern of use of pointers that avoids dangling references as well as storage leaks, by providing safe, immediate, automatic reclamation of storage rather than relying on unchecked deallocation, while also not having to fall back on the time and space vagaries of garbage collection. You might also want to read about how Ada/SPARK does safe pointers. An older article that may be of interest: https://blog.adacore.com/using-pointers-in-spark https://blog.adacore.com/using-pointers-in-spark. Check out https://docs.adacore.com/spark2014-docs/html/ug/en/source/access.html https://docs.adacore.com/spark2014-docs/html/ug/en/source/ac... as well, there is a section named "Deallocation". GNATprove guarantees the absence of memory leak (pretty good, right?) in the code shown under that section. This is how the code looks like: with Ada.Unchecked_Deallocation; procedure Test is type Int_Ptr is access Integer; procedure Free is new Ada.Unchecked_Deallocation (Object => Integer, Name => Int_Ptr); X : Int_Ptr := new Integer'(10); Y : Int_Ptr; begin Y := X; Free (Y); end Test; GNATprove output: test.adb:8:04: info: absence of memory leak at end of scope proved test.adb:9:04: info: initialization of "Y" proved test.adb:9:04: info: absence of memory leak at end of scope proved test.adb:11:06: info: absence of memory leak proved
- devit 5y ago
  Does that proposal allow to express anything that can be expressed in Rust? That seems quite unlikely given the lack of syntax for lifetimes. It's still in theory possible to infer them, but that would result in API instability and hard to decipher error messages. Can you for instance have a function that given a reference to an hash table and a reference to a key returns a reference to the value corresponding to a key equal to the given one? (this requires the return value lifetime to be the same as the hash table lifetime, while the search key lifetime is unrelated) Can you refactor code that takes multiple parameters by reference to taking by value a single structure including those parameters as fields with independent lifetimes?

by devit 5y ago

No, Ada has no lifetimes and borrow checking and thus cannot possibly offer the same expressiveness as Rust while supporting safe memory deallocation without garbage collection.

pjmlp 5y ago

That is why SPARK exists, and RAII offers safe memory deallocation. Ada never used GC, although Ada 83 allowed for optional implementation, that no compiler ever made use of, thus it was removed from Ada standard in the 2005 revision.

johnisgood 5y ago

You may want to read https://www.adacore.com/uploads/techPapers/Safe-Dynamic-Memory-Management-in-Ada-and-SPARK.pdf https://www.adacore.com/uploads/techPapers/Safe-Dynamic-Memo.... It talks plenty about lifetimes and borrowing. It even mentions Rust (and ParaSail). > The goal is to allow a pattern of use of pointers that avoids dangling references as well as storage leaks, by providing safe, immediate, automatic reclamation of storage rather than relying on unchecked deallocation, while also not having to fall back on the time and space vagaries of garbage collection. You might also want to read about how Ada/SPARK does safe pointers. An older article that may be of interest: https://blog.adacore.com/using-pointers-in-spark https://blog.adacore.com/using-pointers-in-spark. Check out https://docs.adacore.com/spark2014-docs/html/ug/en/source/access.html https://docs.adacore.com/spark2014-docs/html/ug/en/source/ac... as well, there is a section named "Deallocation". GNATprove guarantees the absence of memory leak (pretty good, right?) in the code shown under that section. This is how the code looks like: with Ada.Unchecked_Deallocation; procedure Test is type Int_Ptr is access Integer; procedure Free is new Ada.Unchecked_Deallocation (Object => Integer, Name => Int_Ptr); X : Int_Ptr := new Integer'(10); Y : Int_Ptr; begin Y := X; Free (Y); end Test; GNATprove output: test.adb:8:04: info: absence of memory leak at end of scope proved test.adb:9:04: info: initialization of "Y" proved test.adb:9:04: info: absence of memory leak at end of scope proved test.adb:11:06: info: absence of memory leak proved

devit 5y ago
Does that proposal allow to express anything that can be expressed in Rust? That seems quite unlikely given the lack of syntax for lifetimes. It's still in theory possible to infer them, but that would result in API instability and hard to decipher error messages. Can you for instance have a function that given a reference to an hash table and a reference to a key returns a reference to the value corresponding to a key equal to the given one? (this requires the return value lifetime to be the same as the hash table lifetime, while the search key lifetime is unrelated) Can you refactor code that takes multiple parameters by reference to taking by value a single structure including those parameters as fields with independent lifetimes?