4 ms·

I don't know Zig, Ada and D very well, but isn't Rust the only language that can guarantee huge amounts of safety with zero runtime overhead due to the burrow c

I don't know Zig, Ada and D very well, but isn't Rust the only language that can guarantee huge amounts of safety with zero runtime overhead due to the burrow checker? I think that is its differenciating property.

rightbyte 5y ago
> zero runtime overhead due to the burrow checker You have to structure the program in a way to make it happy, though. Which is not zero runtime overhead compared to a wild west program.
pjmlp 5y ago
Nope, Rust still cannot provide formal proofs Ada/SPARK style, and using String, Vec, Rc, Arc, RefCell imposes just runtime checks as other type safe systems languages.
johnisgood 5y ago
No, you can guarantee much more with regarding to safety using Ada/SPARK. I have a table somewhere. So if you want safety guarantees, it is Ada/SPARK all the way. Check out https://blog.adacore.com https://blog.adacore.com. I cannot emphasize it enough: if people really wanted so much safety, they would have chosen Ada/SPARK. I also find Ada easier to read and write than Rust. I know C, OCaml, Erlang, Forth, and Factor, yet I have difficulties with Rust. Am I really that bad of a programmer? Welp, at least I know Ada and I can write actually super safe stuff. :P
- lionkor 5y ago
  "I think Ada/SPARK needs to seriously be considered for a lot more projects. Maybe we need better tooling, but still".unwrap().unwrap().unwrap()
  - johnisgood 5y ago
    It has a package manager now! :D Anyways, there are some things that could make Ada/SPARK more desirable but it has nothing to do with the language itself. :(
- 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
- moltonel3x 5y ago
  A lot of those guarantees are only available in the alloc-free subset of Ada, which make them much less attractive. The devil is in the details, making Ada guarantees not always better than Rust ones.
- _flux 5y ago
  Hm, so can Ada/SPARK bring the same memory safety/data race guarantees to the table as Rust, yet not being more difficult to express and maintain those guarantees? I'm not familiar with the language.

rightbyte 5y ago

> zero runtime overhead due to the burrow checker You have to structure the program in a way to make it happy, though. Which is not zero runtime overhead compared to a wild west program.

pjmlp 5y ago

Nope, Rust still cannot provide formal proofs Ada/SPARK style, and using String, Vec, Rc, Arc, RefCell imposes just runtime checks as other type safe systems languages.

johnisgood 5y ago

No, you can guarantee much more with regarding to safety using Ada/SPARK. I have a table somewhere. So if you want safety guarantees, it is Ada/SPARK all the way. Check out https://blog.adacore.com https://blog.adacore.com. I cannot emphasize it enough: if people really wanted so much safety, they would have chosen Ada/SPARK. I also find Ada easier to read and write than Rust. I know C, OCaml, Erlang, Forth, and Factor, yet I have difficulties with Rust. Am I really that bad of a programmer? Welp, at least I know Ada and I can write actually super safe stuff. :P

lionkor 5y ago
"I think Ada/SPARK needs to seriously be considered for a lot more projects. Maybe we need better tooling, but still".unwrap().unwrap().unwrap()
- johnisgood 5y ago
  It has a package manager now! :D Anyways, there are some things that could make Ada/SPARK more desirable but it has nothing to do with the language itself. :(
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
moltonel3x 5y ago
A lot of those guarantees are only available in the alloc-free subset of Ada, which make them much less attractive. The devil is in the details, making Ada guarantees not always better than Rust ones.
_flux 5y ago
Hm, so can Ada/SPARK bring the same memory safety/data race guarantees to the table as Rust, yet not being more difficult to express and maintain those guarantees? I'm not familiar with the language.