14 ms·

How does Ada's memory safety compare against Rust?

166 points by pabs3 2y ago

deleted 2y ago
[deleted]
ajxs 2y ago
Author here: Thank you so much for posting! Happy to answer any questions anyone might have about the article.
- valorzard 2y ago
  Do you think Ada would be good for game development? My main interest in the new wave of low level languages like Rust, Zig and Odin is to see which one would be good for game dev. Out of all of them, the best would probably be Rust (great ecosystem) and Odin (the designer behind Odin is literally a game dev iirc)
  - ajxs 2y ago
    I've never done it myself, but I know it's possible! The GetIntoGameDev Youtube channel has recently done a few videos on the subject[0]. 0: https://www.youtube.com/watch?v=HZSvlaQ2uHI https://www.youtube.com/watch?v=HZSvlaQ2uHI
  - MrVandemar 2y ago
    I think there's a roguelike on steam maybe that is written in Ada.
bawolff 2y ago
I don't program in rust or ada, however it seems like such a comparison is missing important details. After all, if memory safety was all that mattered we'd all be using python. The thing that gets people excited about rust is not just memory safety but the tradeoffs taken to make that happen.
- ajxs 2y ago
  I look at the problem the other way around: There are certain domains that significantly constrain the choice of programming language, for reasons like compatibility, or performance. If you're already limited to a small set of statically-compiled 'systems languages' like C, Ada, Rust, etc, then memory-safety is a secondary factor that will really influence your choice of which systems programming language you use.
- pjmlp 2y ago
  What got Rust adoption if anything was human factor, most folks adopting it never programmed in Ada, Object Pascal, Modula-2, Delphi,... They weren't even born when we were using them, or if they were their toys were actually toys not systems programming languages. Rust was their first encounter with systems programming, and Standard ML linage, after lots of Python, Ruby and JavaScript, and most likely never seen anything else other than C and C++. Most likely that also believe the fairy tale of C being the very first systems programming language.
  - dakom 2y ago
    I'd agree it's largely the human factor, but maybe from a different angle. Rust has got the "there's a crate for that" factor, like JavaScript, which helps onboard people who are afraid of getting stuck writing everything from scratch. For example, serde (and serde_json, toml, etc.) is a gamechanger, as is tracing, reqwest, and many others. So, maybe less about the language itself for many people, but more about the human factor of overcoming fear of being stuck on an island
  - IshKebab 2y ago
    I'm not sure what point you're trying to make. Do you think Object Pascal is as good as Rust?
    - pjmlp 2y ago
      Nope, but definitly better than C in regards to safety in systems programming.
mustache_kimono 2y ago
Very interesting and timely especially since I see the following so often: > Why wouldn’t the Linux kernel team choose Ada instead of Rust? To which I say: Ada doesn't have a large user base beyond DOD projects. Virtually no greenfield projects except for DOD. Whereas there has been a Cambrian explosion of Unix kernels/tools/servers written in Rust. More generally, these questions of the form "Why are you ignoring X?" where X is Ada or Zig or C++ are really "Why didn't you write/don't you rewrite this in Rust?" by a different name. And my/that answer goes both ways. Notably, Roc recently has stated it is moving away from Rust. Ghostty uses Zig because Mitchell Hashimoto doesn't like Rust. But the answer is always someone has to show up and do the work, usually because they like doing the work in some language. So -- it's okay to like the project strictly because of the language chosen. That being said -- I'm super interested in the more technical differences.
- deleted 2y ago
  [deleted]
- ajxs 2y ago
  The history of computing has many examples of products and languages winning out over technically superior alternatives for non-technical reasons. Like Linux gaining a lot of momentum because of the BSD lawsuit. This[0] is one of my favourite comments on HN. It shows us one of the paths not taken in the evolution of operating systems. > It's okay to like the project strictly because of the language chosen. I think that the massive groundswell of interest around Rust will end up being positive overall. At this point I can't see us going back to the way things were. I can't imagine any new systems programming languages gaining traction that aren't at least as safe as Rust. 0: https://news.ycombinator.com/item?id=32604842 https://news.ycombinator.com/item?id=32604842
  - bigstrat2003 2y ago
    That comment was great. It's so hard for me (raised on Windows and now immersed in Linux) to imagine something so foreign to the OS paradigms I'm used to. It just goes to show how much the things you are used to can limit your thinking.
pjmlp 2y ago
Directly using Unchecked_Deallocation is frowned upon, either use ControlledTypes (which the article mentions), or Bound/Unbounded Collections (which the article misses). Using it directly is similar to the usual discussion of using unsafe in Rust for double linked lists. As of Ada 202x, SPARK covers most of the language, no longer a subset, and also does affine types, aka borrow checking.
- ajxs 2y ago
  > Directly using Unchecked_Deallocation is frowned upon... This is true. I admit that I didn't really acknowledge this in the article. I personally don't really like the Ada community's consensus on this matter. In many applications 'let memory leak and let the OS sort it out' just won't cut it. It's true that you can use controlled types for everything, but isn't this just moving the Unchecked_Deallocation somewhere out of sight? Also, if I'd have written 'You can't leak memory in Ada if you stick to using collections', wouldn't that just be like saying 'You can't leak memory in C++ if you stick to using the STL'? The point of the article was to show what Ada and Rust do to outrightly prevent you from shooting yourself in the foot, at the core language level. There's a lot of misconceptions floating around the Ada community about memory being freed automatically when it goes out of scope, which I think have stemmed from the ARM leaving open the possibility for a compiler to implement its own GC. Admittedly even I was misinformed. In my defence, nearly all the Ada I write is for bare metal, and never touches the heap at all.
  - pjmlp 2y ago
    > ...'let memory leak and let the OS sort it out'.. I wouldn't be surprise to hear this from C or C++ folks, never heard this in Ada circles, there is always that missile meme going around, and I happened in the past to occasionally drop into FOSDEM Ada's rooms. Speaking of which, "Memory Management with Ada 2012 from FOSDEM 2016" https://archive.fosdem.org/2016/schedule/event/ada_memory/ https://archive.fosdem.org/2016/schedule/event/ada_memory/ > Also, if I'd have written 'You can't leak memory in Ada if you stick to using collections', wouldn't that just be like saying 'You can't leak memory in C++ if you stick to using the STL'? The point of the article was to show what Ada and Rust do to outrightly prevent you from shooting yourself in the foot, at the core language level. A programming language is seldom used without its standard library, I don't care what a plain grammar + related semantics check offer, if there is nothing on the standard library, IDE tooling, libraries to chose from. Otherwise than you should also do a comparisasion using no_std against Ravenscar profile. And yes, unless you are using a C++ compiler that offers the option to harden its standard library, you are going to some surprises, starting by having to use at() instead of operator[]() for bounds checking, and even with hardened one, stuff like use-after-free/move only when using a good IDE like VC++/Clion or static/dynamic analysis tooling.
deleted 2y ago
[deleted]
trott 2y ago
> but Ada's real strengths lie elsewhere. Its strong typing, Ada is not actually type-safe: https://www.enyo.de/fw/notes/ada-type-safety.html https://www.enyo.de/fw/notes/ada-type-safety.html
- adrian_b 2y ago
  As explained at your link, the example program that is not type-safe is based on a mistake of the 1983 Ada standard regarding the use of "aliased", which has been removed by a later Technical Corrigendum, where the program demonstrated at your link is explicitly classified as erroneous, so any compliant Ada compiler should fail to compile it. As also explained at your link, the same type-safety breaking technique works in unsafe Rust. Both "unchecked" Ada and "unsafe" Rust do not provide type safety, while the safe subsets of the languages provide it.
  - trott 2y ago
    > a mistake of the 1983 Ada standard ... which has been removed The article was written in 2011, and the trick still seems to work in a 2024 version of GNAT. > Both "unchecked" Ada and "unsafe" Rust But the `Conversion` function isn't using `Unchecked_*`. That's the point of the article. The type safety hole is in "safe" Ada.
    - deleted 2y ago
      [deleted]
    - deleted 2y ago
      [deleted]
  - steveklabnik 2y ago
    While that was apparently true in 2015, it doesn't work on today's Rust: https://play.rust-lang.org/?version=stable&mode=debug&edition=2021&gist=429be7537352f4d3deee66294e263e2e https://play.rust-lang.org/?version=stable&mode=debug&editio... I'm not sure what the difference was, given that the representations haven't changed, and I'm doing this without invoking the optimizer. EDIT: I had issues with Miri so I dug into the MIR myself: let uncopied : *const Uncopyable<*const B> = match magic { Magic::B(b) => &raw const b, StorageLive(_4); StorageLive(_5); _5 = move ((_3 as B).0: Uncopyable<*const B>); _4 = &raw const _5; StorageDead(_5); _3 is magic, _4 is uncopied, and 5 is b. move here is like ptr::read, which means that uncopied points to a copy of magic, not aliasing magic, and is dangling. Because this is UB, it gets optimized straight into the panic. After I figured that out, miri started working, I must have made a mistake earlier. It will tell us the same thing: test test ... error: Undefined Behavior: memory access failed: alloc113986 has been freed, so this pointer is dangling --> src/lib.rs:24:13 | 24 | assert!((*uncopied).value != std::ptr::null()); | ^^^^^^^^^^^^^^^^^ memory access failed: alloc113986 has been freed, so this pointer is dangling | = help: this indicates a bug in the program: it performed an invalid operation, and caused Undefined Behavior = help: see https://doc.rust-lang.org/nightly/reference/behavior-considered-undefined.html for further information help: alloc113986 was allocated here: --> src/lib.rs:18:16 | 18 | Magic::B(b) => &b, | ^ help: alloc113986 was deallocated here: --> src/lib.rs:18:23 | 18 | Magic::B(b) => &b, | ^ = note: BACKTRACE (of the first span) on thread `test`: = note: inside `magic::<&str, &u8>` at src/lib.rs:24:13: 24:30 note: inside `test` --> src/lib.rs:36:5 | 36 | magic::<&str, &u8>("magic string"); | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ note: inside closure --> src/lib.rs:35:10 | 34 | #[test] | ------- in this procedural macro expansion 35 | fn test() { | ^ = note: this error originates in the attribute macro `test` (in Nightly builds, run with -Z macro-backtrace for more info) This code started failing in Rust 1.12, when MIR happened, so that's exactly my guess as to what fixed it. Funny enough, if we take the critique in the forum as correct, and try with a union: https://play.rust-lang.org/?version=stable&mode=debug&edition=2021&gist=9ed6584d7a54a95de0d831a17683ea8f https://play.rust-lang.org/?version=stable&mode=debug&editio... Rust will: 1. force us to use ManuallyDrop 2. the API makes this move explicit, and we get a compile-time error!
roydivision 2y ago
I thought this would be comparing Rust to Ada Lovelace's code... And I've coded in Ada...
renox 2y ago
> [about Ada] You never miss worrying about whether a parameter is passed by value or reference Uh? I thought that Ada suffered from the "aliasing issue"(1): given that the compiler choose whether to copy or alias, there is a risk that the semantic of your program change when the compiler/optimisation change, am I wrong? 1: if you have a function with two parameters, one "in" and the other "inout" and you pass the same variable to the two parameters.
- tgv 2y ago
  You have to specifically state when parameters can be aliased. Otherwise, the compiler forbids it.
  - renox 2y ago
    Well godbolt doesn't think so.. 1) this example has an aliasing, no compiler error. https://godbolt.org/z/hzWfj37ef https://godbolt.org/z/hzWfj37ef 2) The output value depends of the size of IntArray! >> with Ada.Text_IO; use Ada.Text_IO; with Ada.Integer_Text_IO; use Ada.Integer_Text_IO; procedure Text is type IntArray is array (1 .. 500) of Integer; type MyStruct is record Value : Integer; A : IntArray := (others => 0); end record; function Compute (Value1 : MyStruct; Value2 : in out MyStruct) return Integer is begin Put_Line ("1 value1=" & Integer'Image(Value1.Value) & " value2=" & Integer'Image(Value2.Value)); Value2.Value := Value2.Value - 1; Put_Line ("2 value1=" & Integer'Image(Value1.Value) & " value2=" & Integer'Image(Value2.Value)); return Value1.Value * 2; end Compute; Value1 : MyStruct := (Value => 10, A => (others => 0)); Value2 : MyStruct := (Value => 20, A => (others => 0)); Result1 : Integer; Result2 : Integer; begin Result1 := Compute(Value1, Value2); Put_Line ("a value1=" & Integer'Image(Value1.Value) & " value2=" & Integer'Image(Value2.Value) & " result1=" & Integer'Image(Result1)); Result2 := Compute(Value1, Value1); Put_Line ("b value1=" & Integer'Image(Value1.Value) & " value2=" & Integer'Image(Value2.Value) & " result2=" & Integer'Image(Result2)); end Text; <<
    - tgv 2y ago
      My Ada is somewhat weak, but IIRC Value2 doesn't alias Value1. The parameters don't work like C. It's more like an assignment once the function returns, although the compiler is free to deviate from that.
Yoric 2y ago
Thank you very much! I have been attempting to compare Ada and Rust for a while, but never got around to doing it quite so much in depth. So, my take on this is that: - out of the box, Rust is distinctly better at memory safety than Ada without SPARK - Ada + SPARK is extremely powerful (but iirc, SPARK doesn't allow compositional reasoning, which makes it harder to use in a crate-based library) - for this specific use case, Rust's error model makes much more sense than Ada's (with or without SPARK) - Ada's tooling to avoid memory allocation remain more powerful in some dimensions than Rust's. Also, I think that we all (should) agree that the move towards memory safety in system-level programming is a very good thing, whether it comes through Rust, Ada, or any other language.
kennysoona 2y ago
The SPARK subset of ADA really seems the best here, but doesn't seem anywhere near as fun to write as Rust, or have anywhere near the amount of libraries available. The community is much smaller also, and I think community counts for a lot here. The takeaway is Rust, really is, really really great. It's fantastic there is so much documentation and such a strong community, and that so many people are invested in writing safe code because it's finally easy to do so.
- tgv 2y ago
  SPARK offers more than Rust, and in my experience, writing Rust isn't fun (either). Rust has more documentation to get you going than Ada, and certainly more than SPARK, as well as a much larger community and more libraries, but the Ada/SPARK community is a nice, helpful bunch.
transpute 2y ago
Ada+Rust (2022), https://blog.adacore.com/adacore-and-ferrous-systems-joining-forces-to-support-rust https://blog.adacore.com/adacore-and-ferrous-systems-joining... > Ferrous Systems and AdaCore are.. joining forces to develop Ferrocene - a safety-qualified Rust toolchain, which is aimed at supporting the needs of various regulated markets, such as automotive, avionics, space, and railway.. qualifying the Ferrocene Rust compiler according to various safety standards.. [including] development and qualification of the necessary dynamic and static analysis tools.. our long-term commitment to Rust and Ada extends to developers who will be using both languages at the same time. We are looking at interoperability between them - including, in particular, the idea of developing bi-directional binding generators. Nvidia uses Ada/SPARK for formally-verified security firmware on RISC-V cores on GPUs [1] and SPDM attestation of devices like GPUs and Infiniband NICs [2]. [1] https://blog.adacore.com/when-formal-verification-with-spark-is-the-strongest-link https://blog.adacore.com/when-formal-verification-with-spark... & https://static.sched.com/hosted_files/riscvsummit2024/fe/Keynote_2024.pdf https://static.sched.com/hosted_files/riscvsummit2024/fe/Key... [2] https://www.adacore.com/papers/nvidia-using-recordflux-and-spark-to-implement-spdm-for-secure-computing https://www.adacore.com/papers/nvidia-using-recordflux-and-s... & https://docs.nvidia.com/networking/display/nvidiadeviceattestationandcorimbasedreferencemeasurementsharingv20 https://docs.nvidia.com/networking/display/nvidiadeviceattes...
vlovich123 2y ago
> Nothing prevents you from writing Ada code that dereferences an access type after it's been freed; However any access dereference triggers a runtime check to ensure it's non-null. Unlike in C, freeing an access type in Ada automatically sets its value to null, and any subsequent attempt to dereference it will raise a Constraint_Error exception, which can be caught and handled. > Ada has its own nomenclature for multithreading: Tasks, and provides its own built-in mechanism for preventing data races between them. Ada's Protected Objects encapsulate data inside an implicit mutex, allowing only one thread access at a time via a public interface. I believe ADA doesn’t have a guarantee that you are accessing data thread safely. And that lack of guarantee is where use-after-free and double-free can hide. Heck, you don’t even need any threading. 1. Create an alias 2. Free the original value 3. Access the alias If I read it correctly, the variable holding the original value is reset to null after a free but the alias can still access freed memory. TLDR: Rust has almost no competitors when it comes to the very robust safety guarantees it makes and none when you combine with the performance niche it services.
- adrian_b 2y ago
  Programming languages where you are not allowed to access directly any shared variables, but only inside protected data structures, so that complete thread safety is enforced, have existed already a half of century ago, e.g. Concurrent Pascal. I have not noticed yet anything innovative in this aspect of Rust. As explained in the article SPARK detects such double free or use after free, even if the standard Ada compiler does not. The separation between Ada and SPARK in the power of detecting unsafe memory uses is just a market segmentation mechanism, not something intrinsic to the Ada language. The SPARK development tools must be bought, while the free Ada development tools have less comprehensive error checking. This is the main disadvantage of Ada vs. Rust. It is a question of money, not of technical qualities.
  - zozbot234 2y ago
    AIUI, SPARK does not use a Rust-like borrow checker: it's based on formal verification which is a lot more difficult to program for, i.e. not really feasible except for smaller programs. This seems to be in sharp contrast to Rust - the safe subset of Rust enforces a set of rules that can actually scale up to larger programs while still preserving safety.

166 points by pabs3 2y ago

deleted 2y ago

[deleted]

ajxs 2y ago

Author here: Thank you so much for posting! Happy to answer any questions anyone might have about the article.

valorzard 2y ago
Do you think Ada would be good for game development? My main interest in the new wave of low level languages like Rust, Zig and Odin is to see which one would be good for game dev. Out of all of them, the best would probably be Rust (great ecosystem) and Odin (the designer behind Odin is literally a game dev iirc)
- ajxs 2y ago
  I've never done it myself, but I know it's possible! The GetIntoGameDev Youtube channel has recently done a few videos on the subject[0]. 0: https://www.youtube.com/watch?v=HZSvlaQ2uHI https://www.youtube.com/watch?v=HZSvlaQ2uHI
- MrVandemar 2y ago
  I think there's a roguelike on steam maybe that is written in Ada.

bawolff 2y ago

I don't program in rust or ada, however it seems like such a comparison is missing important details. After all, if memory safety was all that mattered we'd all be using python. The thing that gets people excited about rust is not just memory safety but the tradeoffs taken to make that happen.

ajxs 2y ago
I look at the problem the other way around: There are certain domains that significantly constrain the choice of programming language, for reasons like compatibility, or performance. If you're already limited to a small set of statically-compiled 'systems languages' like C, Ada, Rust, etc, then memory-safety is a secondary factor that will really influence your choice of which systems programming language you use.
pjmlp 2y ago
What got Rust adoption if anything was human factor, most folks adopting it never programmed in Ada, Object Pascal, Modula-2, Delphi,... They weren't even born when we were using them, or if they were their toys were actually toys not systems programming languages. Rust was their first encounter with systems programming, and Standard ML linage, after lots of Python, Ruby and JavaScript, and most likely never seen anything else other than C and C++. Most likely that also believe the fairy tale of C being the very first systems programming language.
- dakom 2y ago
  I'd agree it's largely the human factor, but maybe from a different angle. Rust has got the "there's a crate for that" factor, like JavaScript, which helps onboard people who are afraid of getting stuck writing everything from scratch. For example, serde (and serde_json, toml, etc.) is a gamechanger, as is tracing, reqwest, and many others. So, maybe less about the language itself for many people, but more about the human factor of overcoming fear of being stuck on an island
- IshKebab 2y ago
  I'm not sure what point you're trying to make. Do you think Object Pascal is as good as Rust?
  - pjmlp 2y ago
    Nope, but definitly better than C in regards to safety in systems programming.

mustache_kimono 2y ago

Very interesting and timely especially since I see the following so often: > Why wouldn’t the Linux kernel team choose Ada instead of Rust? To which I say: Ada doesn't have a large user base beyond DOD projects. Virtually no greenfield projects except for DOD. Whereas there has been a Cambrian explosion of Unix kernels/tools/servers written in Rust. More generally, these questions of the form "Why are you ignoring X?" where X is Ada or Zig or C++ are really "Why didn't you write/don't you rewrite this in Rust?" by a different name. And my/that answer goes both ways. Notably, Roc recently has stated it is moving away from Rust. Ghostty uses Zig because Mitchell Hashimoto doesn't like Rust. But the answer is always someone has to show up and do the work, usually because they like doing the work in some language. So -- it's okay to like the project strictly because of the language chosen. That being said -- I'm super interested in the more technical differences.

deleted 2y ago
[deleted]
ajxs 2y ago
The history of computing has many examples of products and languages winning out over technically superior alternatives for non-technical reasons. Like Linux gaining a lot of momentum because of the BSD lawsuit. This[0] is one of my favourite comments on HN. It shows us one of the paths not taken in the evolution of operating systems. > It's okay to like the project strictly because of the language chosen. I think that the massive groundswell of interest around Rust will end up being positive overall. At this point I can't see us going back to the way things were. I can't imagine any new systems programming languages gaining traction that aren't at least as safe as Rust. 0: https://news.ycombinator.com/item?id=32604842 https://news.ycombinator.com/item?id=32604842
- bigstrat2003 2y ago
  That comment was great. It's so hard for me (raised on Windows and now immersed in Linux) to imagine something so foreign to the OS paradigms I'm used to. It just goes to show how much the things you are used to can limit your thinking.

pjmlp 2y ago

Directly using Unchecked_Deallocation is frowned upon, either use ControlledTypes (which the article mentions), or Bound/Unbounded Collections (which the article misses). Using it directly is similar to the usual discussion of using unsafe in Rust for double linked lists. As of Ada 202x, SPARK covers most of the language, no longer a subset, and also does affine types, aka borrow checking.

ajxs 2y ago
> Directly using Unchecked_Deallocation is frowned upon... This is true. I admit that I didn't really acknowledge this in the article. I personally don't really like the Ada community's consensus on this matter. In many applications 'let memory leak and let the OS sort it out' just won't cut it. It's true that you can use controlled types for everything, but isn't this just moving the Unchecked_Deallocation somewhere out of sight? Also, if I'd have written 'You can't leak memory in Ada if you stick to using collections', wouldn't that just be like saying 'You can't leak memory in C++ if you stick to using the STL'? The point of the article was to show what Ada and Rust do to outrightly prevent you from shooting yourself in the foot, at the core language level. There's a lot of misconceptions floating around the Ada community about memory being freed automatically when it goes out of scope, which I think have stemmed from the ARM leaving open the possibility for a compiler to implement its own GC. Admittedly even I was misinformed. In my defence, nearly all the Ada I write is for bare metal, and never touches the heap at all.
- pjmlp 2y ago
  > ...'let memory leak and let the OS sort it out'.. I wouldn't be surprise to hear this from C or C++ folks, never heard this in Ada circles, there is always that missile meme going around, and I happened in the past to occasionally drop into FOSDEM Ada's rooms. Speaking of which, "Memory Management with Ada 2012 from FOSDEM 2016" https://archive.fosdem.org/2016/schedule/event/ada_memory/ https://archive.fosdem.org/2016/schedule/event/ada_memory/ > Also, if I'd have written 'You can't leak memory in Ada if you stick to using collections', wouldn't that just be like saying 'You can't leak memory in C++ if you stick to using the STL'? The point of the article was to show what Ada and Rust do to outrightly prevent you from shooting yourself in the foot, at the core language level. A programming language is seldom used without its standard library, I don't care what a plain grammar + related semantics check offer, if there is nothing on the standard library, IDE tooling, libraries to chose from. Otherwise than you should also do a comparisasion using no_std against Ravenscar profile. And yes, unless you are using a C++ compiler that offers the option to harden its standard library, you are going to some surprises, starting by having to use at() instead of operator[]() for bounds checking, and even with hardened one, stuff like use-after-free/move only when using a good IDE like VC++/Clion or static/dynamic analysis tooling.

deleted 2y ago

[deleted]

trott 2y ago

> but Ada's real strengths lie elsewhere. Its strong typing, Ada is not actually type-safe: https://www.enyo.de/fw/notes/ada-type-safety.html https://www.enyo.de/fw/notes/ada-type-safety.html

adrian_b 2y ago
As explained at your link, the example program that is not type-safe is based on a mistake of the 1983 Ada standard regarding the use of "aliased", which has been removed by a later Technical Corrigendum, where the program demonstrated at your link is explicitly classified as erroneous, so any compliant Ada compiler should fail to compile it. As also explained at your link, the same type-safety breaking technique works in unsafe Rust. Both "unchecked" Ada and "unsafe" Rust do not provide type safety, while the safe subsets of the languages provide it.
- trott 2y ago
  > a mistake of the 1983 Ada standard ... which has been removed The article was written in 2011, and the trick still seems to work in a 2024 version of GNAT. > Both "unchecked" Ada and "unsafe" Rust But the `Conversion` function isn't using `Unchecked_*`. That's the point of the article. The type safety hole is in "safe" Ada.
  - deleted 2y ago
    [deleted]
  - deleted 2y ago
    [deleted]
- steveklabnik 2y ago
  While that was apparently true in 2015, it doesn't work on today's Rust: https://play.rust-lang.org/?version=stable&mode=debug&edition=2021&gist=429be7537352f4d3deee66294e263e2e https://play.rust-lang.org/?version=stable&mode=debug&editio... I'm not sure what the difference was, given that the representations haven't changed, and I'm doing this without invoking the optimizer. EDIT: I had issues with Miri so I dug into the MIR myself: let uncopied : *const Uncopyable<*const B> = match magic { Magic::B(b) => &raw const b, StorageLive(_4); StorageLive(_5); _5 = move ((_3 as B).0: Uncopyable<*const B>); _4 = &raw const _5; StorageDead(_5); _3 is magic, _4 is uncopied, and 5 is b. move here is like ptr::read, which means that uncopied points to a copy of magic, not aliasing magic, and is dangling. Because this is UB, it gets optimized straight into the panic. After I figured that out, miri started working, I must have made a mistake earlier. It will tell us the same thing: test test ... error: Undefined Behavior: memory access failed: alloc113986 has been freed, so this pointer is dangling --> src/lib.rs:24:13 | 24 | assert!((*uncopied).value != std::ptr::null()); | ^^^^^^^^^^^^^^^^^ memory access failed: alloc113986 has been freed, so this pointer is dangling | = help: this indicates a bug in the program: it performed an invalid operation, and caused Undefined Behavior = help: see https://doc.rust-lang.org/nightly/reference/behavior-considered-undefined.html for further information help: alloc113986 was allocated here: --> src/lib.rs:18:16 | 18 | Magic::B(b) => &b, | ^ help: alloc113986 was deallocated here: --> src/lib.rs:18:23 | 18 | Magic::B(b) => &b, | ^ = note: BACKTRACE (of the first span) on thread `test`: = note: inside `magic::<&str, &u8>` at src/lib.rs:24:13: 24:30 note: inside `test` --> src/lib.rs:36:5 | 36 | magic::<&str, &u8>("magic string"); | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ note: inside closure --> src/lib.rs:35:10 | 34 | #[test] | ------- in this procedural macro expansion 35 | fn test() { | ^ = note: this error originates in the attribute macro `test` (in Nightly builds, run with -Z macro-backtrace for more info) This code started failing in Rust 1.12, when MIR happened, so that's exactly my guess as to what fixed it. Funny enough, if we take the critique in the forum as correct, and try with a union: https://play.rust-lang.org/?version=stable&mode=debug&edition=2021&gist=9ed6584d7a54a95de0d831a17683ea8f https://play.rust-lang.org/?version=stable&mode=debug&editio... Rust will: 1. force us to use ManuallyDrop 2. the API makes this move explicit, and we get a compile-time error!

roydivision 2y ago

I thought this would be comparing Rust to Ada Lovelace's code... And I've coded in Ada...

renox 2y ago

> [about Ada] You never miss worrying about whether a parameter is passed by value or reference Uh? I thought that Ada suffered from the "aliasing issue"(1): given that the compiler choose whether to copy or alias, there is a risk that the semantic of your program change when the compiler/optimisation change, am I wrong? 1: if you have a function with two parameters, one "in" and the other "inout" and you pass the same variable to the two parameters.

tgv 2y ago
You have to specifically state when parameters can be aliased. Otherwise, the compiler forbids it.
- renox 2y ago
  Well godbolt doesn't think so.. 1) this example has an aliasing, no compiler error. https://godbolt.org/z/hzWfj37ef https://godbolt.org/z/hzWfj37ef 2) The output value depends of the size of IntArray! >> with Ada.Text_IO; use Ada.Text_IO; with Ada.Integer_Text_IO; use Ada.Integer_Text_IO; procedure Text is type IntArray is array (1 .. 500) of Integer; type MyStruct is record Value : Integer; A : IntArray := (others => 0); end record; function Compute (Value1 : MyStruct; Value2 : in out MyStruct) return Integer is begin Put_Line ("1 value1=" & Integer'Image(Value1.Value) & " value2=" & Integer'Image(Value2.Value)); Value2.Value := Value2.Value - 1; Put_Line ("2 value1=" & Integer'Image(Value1.Value) & " value2=" & Integer'Image(Value2.Value)); return Value1.Value * 2; end Compute; Value1 : MyStruct := (Value => 10, A => (others => 0)); Value2 : MyStruct := (Value => 20, A => (others => 0)); Result1 : Integer; Result2 : Integer; begin Result1 := Compute(Value1, Value2); Put_Line ("a value1=" & Integer'Image(Value1.Value) & " value2=" & Integer'Image(Value2.Value) & " result1=" & Integer'Image(Result1)); Result2 := Compute(Value1, Value1); Put_Line ("b value1=" & Integer'Image(Value1.Value) & " value2=" & Integer'Image(Value2.Value) & " result2=" & Integer'Image(Result2)); end Text; <<
  - tgv 2y ago
    My Ada is somewhat weak, but IIRC Value2 doesn't alias Value1. The parameters don't work like C. It's more like an assignment once the function returns, although the compiler is free to deviate from that.

Yoric 2y ago

Thank you very much! I have been attempting to compare Ada and Rust for a while, but never got around to doing it quite so much in depth. So, my take on this is that: - out of the box, Rust is distinctly better at memory safety than Ada without SPARK - Ada + SPARK is extremely powerful (but iirc, SPARK doesn't allow compositional reasoning, which makes it harder to use in a crate-based library) - for this specific use case, Rust's error model makes much more sense than Ada's (with or without SPARK) - Ada's tooling to avoid memory allocation remain more powerful in some dimensions than Rust's. Also, I think that we all (should) agree that the move towards memory safety in system-level programming is a very good thing, whether it comes through Rust, Ada, or any other language.

kennysoona 2y ago

The SPARK subset of ADA really seems the best here, but doesn't seem anywhere near as fun to write as Rust, or have anywhere near the amount of libraries available. The community is much smaller also, and I think community counts for a lot here. The takeaway is Rust, really is, really really great. It's fantastic there is so much documentation and such a strong community, and that so many people are invested in writing safe code because it's finally easy to do so.

tgv 2y ago
SPARK offers more than Rust, and in my experience, writing Rust isn't fun (either). Rust has more documentation to get you going than Ada, and certainly more than SPARK, as well as a much larger community and more libraries, but the Ada/SPARK community is a nice, helpful bunch.

transpute 2y ago

Ada+Rust (2022), https://blog.adacore.com/adacore-and-ferrous-systems-joining-forces-to-support-rust https://blog.adacore.com/adacore-and-ferrous-systems-joining... > Ferrous Systems and AdaCore are.. joining forces to develop Ferrocene - a safety-qualified Rust toolchain, which is aimed at supporting the needs of various regulated markets, such as automotive, avionics, space, and railway.. qualifying the Ferrocene Rust compiler according to various safety standards.. [including] development and qualification of the necessary dynamic and static analysis tools.. our long-term commitment to Rust and Ada extends to developers who will be using both languages at the same time. We are looking at interoperability between them - including, in particular, the idea of developing bi-directional binding generators. Nvidia uses Ada/SPARK for formally-verified security firmware on RISC-V cores on GPUs [1] and SPDM attestation of devices like GPUs and Infiniband NICs [2]. [1] https://blog.adacore.com/when-formal-verification-with-spark-is-the-strongest-link https://blog.adacore.com/when-formal-verification-with-spark... & https://static.sched.com/hosted_files/riscvsummit2024/fe/Keynote_2024.pdf https://static.sched.com/hosted_files/riscvsummit2024/fe/Key... [2] https://www.adacore.com/papers/nvidia-using-recordflux-and-spark-to-implement-spdm-for-secure-computing https://www.adacore.com/papers/nvidia-using-recordflux-and-s... & https://docs.nvidia.com/networking/display/nvidiadeviceattestationandcorimbasedreferencemeasurementsharingv20 https://docs.nvidia.com/networking/display/nvidiadeviceattes...

vlovich123 2y ago

> Nothing prevents you from writing Ada code that dereferences an access type after it's been freed; However any access dereference triggers a runtime check to ensure it's non-null. Unlike in C, freeing an access type in Ada automatically sets its value to null, and any subsequent attempt to dereference it will raise a Constraint_Error exception, which can be caught and handled. > Ada has its own nomenclature for multithreading: Tasks, and provides its own built-in mechanism for preventing data races between them. Ada's Protected Objects encapsulate data inside an implicit mutex, allowing only one thread access at a time via a public interface. I believe ADA doesn’t have a guarantee that you are accessing data thread safely. And that lack of guarantee is where use-after-free and double-free can hide. Heck, you don’t even need any threading. 1. Create an alias 2. Free the original value 3. Access the alias If I read it correctly, the variable holding the original value is reset to null after a free but the alias can still access freed memory. TLDR: Rust has almost no competitors when it comes to the very robust safety guarantees it makes and none when you combine with the performance niche it services.

adrian_b 2y ago
Programming languages where you are not allowed to access directly any shared variables, but only inside protected data structures, so that complete thread safety is enforced, have existed already a half of century ago, e.g. Concurrent Pascal. I have not noticed yet anything innovative in this aspect of Rust. As explained in the article SPARK detects such double free or use after free, even if the standard Ada compiler does not. The separation between Ada and SPARK in the power of detecting unsafe memory uses is just a market segmentation mechanism, not something intrinsic to the Ada language. The SPARK development tools must be bought, while the free Ada development tools have less comprehensive error checking. This is the main disadvantage of Ada vs. Rust. It is a question of money, not of technical qualities.
- zozbot234 2y ago
  AIUI, SPARK does not use a Rust-like borrow checker: it's based on formal verification which is a lot more difficult to program for, i.e. not really feasible except for smaller programs. This seems to be in sharp contrast to Rust - the safe subset of Rust enforces a set of rules that can actually scale up to larger programs while still preserving safety.