4 ms·

I didn't watch the video but I read the pdf transcript. I noticed that the contract example (if x > 50 then x+50 > 100) can fail because of integer overflow.

I didn't watch the video but I read the pdf transcript. I noticed that the contract example (if x > 50 then x+50 > 100) can fail because of integer overflow. This is an area that Ada seems to take much more seriously than Rust does. Anyone know what happened with Adacore and Ferrocene? Are they no longer working together? It sounded like a good collaboration earlier on, given the Rust juggernaut. Also I notice no mention of anything like SPARK for Rust. I still feel like Rust and Ada are designed for differing domains. The archetypal Ada app in particular might malloc some memory (and possibly fail) during an initialization phase, but post-initialization, must never fail, which for among other things basically says never use malloc. The post initialization part is basically a control loop using those fixed buffers to keep a jet engine spinning or whatever. Rust's archetype application on the other hand is a web browser: tons of dynamic allocation, possible memory exhaustion depending on what the user tries to do, and the requirement is to never fail ungracefully, as opposed to never failing at all. "Never fail at all" is not exactly more stringent or complicated: it just means you're not allowed to even attempt certain things, because they might fail.

eschaton 2y ago
Ada definitely targets the same domain as Rust, it just _also_ targets additional domains like low level control systems. It has a lot of flexibility and is quite a good language design that people seem irrationally prejudiced against because it has Algol/Pascal-flavored syntax instead of C-flavored syntax.
- throwaway81523 2y ago
  From what I can tell, trying to write a browser in Ada would be madness. Ada's memory management stuff is very primitive compared to Rust's. That may change as Ada keeps evolving, of course.
  - waste_monk 2y ago
    It has historically been solved in different ways [1] :) Unfortunately most people would not be happy taking the same approach to their web browser. [1] https://devblogs.microsoft.com/oldnewthing/20180228-00/?p=98125 https://devblogs.microsoft.com/oldnewthing/20180228-00/?p=98... where the subject post was from comp.lang.ada.
cashsterling 2y ago
Rust has functionality in the std lib for saturating arithmetic (and other kinds of arithmetic via crates) so that calculations saturate rather than overflow, etc. https://doc.rust-lang.org/nightly/std/?search=saturating https://doc.rust-lang.org/nightly/std/?search=saturating
- throwaway81523 2y ago
  From what I can tell, you have to do special crap in Rust to deal with overflow. Saturating is almost never what you want with integers. "Integers" itself, the math term, denotes the infinite set 1,2,3... and while computer arithmetic is necessary limited to a finite fragment, computer integer calculations should always give the same result that you would get using the unbounded mathematical integers. When that doesn't work, you should get an overflow exception, similar to running out of memory. In Ada, I think the relevant exception is Constraint_Error, but I don't think Rust has a way to do that. By "that" I mean ordinary addition like "a+b" where and b are i32 variables, gets overflow checked without having to call checked_add(a,b) instead of a+b. Is that mistaken?
  - steveklabnik 2y ago
    > In Ada, I think the relevant exception is Constraint_Error, but I don't think Rust has a way to do that. By "that" I mean ordinary addition like "a+b" where and b are i32 variables, gets overflow checked without having to call checked_add(a,b) instead of a+b. Is that mistaken? So, this answer to this is yes and no, in different senses. So first of all, Constraint_Error is an exception, and Rust doesn't use exceptions for error handling like this. It does have panics, but a Rust-native API wouldn't use a panic in this situation. and so the type signature of checked_add looks like this, for i8: pub const fn checked_add(self, rhs: i8) -> Option<i8> This returns an Option type, which you can than handle as you wish. So it's true, you invoke this like a.checked_add(b) Now, there are two other common semantics for checked addition: saturating, and wrapping. They look like this: a.saturating_add(b) a.wrapping_add(b) Okay. At this point we can actually get into the interesting part: yes, typing this is not as nice as a + b. However, for both saturating and wrapping addition, there are wrapper types: use std::num::Saturating; let max = Saturating(u32::MAX); let one = Saturating(1u32); max + one to get a u32 back out, you use .0, since this is just a wrapper struct: (max + one).0 So! What about checked? Well... there isn't one. It appears that the reason why is that it was proposed, and then there wasn't a lot of enthusiasm, so it got closed. What's interesting is that Saturating was in that RFC as well, but I guess it made it in later. There exist packages like https://crates.io/crates/checked https://crates.io/crates/checked so if you really want this anyway, you can still have it.

eschaton 2y ago

Ada definitely targets the same domain as Rust, it just _also_ targets additional domains like low level control systems. It has a lot of flexibility and is quite a good language design that people seem irrationally prejudiced against because it has Algol/Pascal-flavored syntax instead of C-flavored syntax.

throwaway81523 2y ago
From what I can tell, trying to write a browser in Ada would be madness. Ada's memory management stuff is very primitive compared to Rust's. That may change as Ada keeps evolving, of course.
- waste_monk 2y ago
  It has historically been solved in different ways [1] :) Unfortunately most people would not be happy taking the same approach to their web browser. [1] https://devblogs.microsoft.com/oldnewthing/20180228-00/?p=98125 https://devblogs.microsoft.com/oldnewthing/20180228-00/?p=98... where the subject post was from comp.lang.ada.

cashsterling 2y ago

Rust has functionality in the std lib for saturating arithmetic (and other kinds of arithmetic via crates) so that calculations saturate rather than overflow, etc. https://doc.rust-lang.org/nightly/std/?search=saturating https://doc.rust-lang.org/nightly/std/?search=saturating

throwaway81523 2y ago
From what I can tell, you have to do special crap in Rust to deal with overflow. Saturating is almost never what you want with integers. "Integers" itself, the math term, denotes the infinite set 1,2,3... and while computer arithmetic is necessary limited to a finite fragment, computer integer calculations should always give the same result that you would get using the unbounded mathematical integers. When that doesn't work, you should get an overflow exception, similar to running out of memory. In Ada, I think the relevant exception is Constraint_Error, but I don't think Rust has a way to do that. By "that" I mean ordinary addition like "a+b" where and b are i32 variables, gets overflow checked without having to call checked_add(a,b) instead of a+b. Is that mistaken?
- steveklabnik 2y ago
  > In Ada, I think the relevant exception is Constraint_Error, but I don't think Rust has a way to do that. By "that" I mean ordinary addition like "a+b" where and b are i32 variables, gets overflow checked without having to call checked_add(a,b) instead of a+b. Is that mistaken? So, this answer to this is yes and no, in different senses. So first of all, Constraint_Error is an exception, and Rust doesn't use exceptions for error handling like this. It does have panics, but a Rust-native API wouldn't use a panic in this situation. and so the type signature of checked_add looks like this, for i8: pub const fn checked_add(self, rhs: i8) -> Option<i8> This returns an Option type, which you can than handle as you wish. So it's true, you invoke this like a.checked_add(b) Now, there are two other common semantics for checked addition: saturating, and wrapping. They look like this: a.saturating_add(b) a.wrapping_add(b) Okay. At this point we can actually get into the interesting part: yes, typing this is not as nice as a + b. However, for both saturating and wrapping addition, there are wrapper types: use std::num::Saturating; let max = Saturating(u32::MAX); let one = Saturating(1u32); max + one to get a u32 back out, you use .0, since this is just a wrapper struct: (max + one).0 So! What about checked? Well... there isn't one. It appears that the reason why is that it was proposed, and then there wasn't a lot of enthusiasm, so it got closed. What's interesting is that Saturating was in that RFC as well, but I guess it made it in later. There exist packages like https://crates.io/crates/checked https://crates.io/crates/checked so if you really want this anyway, you can still have it.