4 ms·

Well, you kind of underline my point: Rust does not encode the difference between "is true" and "was, at least briefly, true" in the type system. You can reach

Well, you kind of underline my point: Rust does not encode the difference between "is true" and "was, at least briefly, true" in the type system. You can reach for other types/abstractions (and whatever data you touch inside the if might also have the borrow checker up in arms), but that above code as written is suspect.

josephcsible 4y ago
> Rust does not encode the difference between "is true" and "was, at least briefly, true" in the type system. Couldn't it encode that by taking advantage of the fact that nobody else can change a variable while you have it mutably borrowed?
- marcosdumay 4y ago
  Isn't that exactly what people do. This thread seems surreal to me. Rust type system does encode exactly what the later comments are complaining that isn't encoded. And you sate what code cares about the variable keeping its value through a code block, between a pair of braces.
  - MauranKilom 4y ago
    What I meant was *For atomics*, rust does not encode the difference between "is true" and "was, at least briefly, true" in the type system. Obviously, rust has many ways to track this kind of distinction in a compile-time manner (and yes, the borrow checker is one of them). That was not in question.
    - marcosdumay 4y ago
      Hum, ok. You don't consider the borrow checker to be part of the type system. Well, it's perfectly fine to disagree on name definitions, but that is some fuzzy and dizzy line. Lifetimes impose themselves together with the static types features all the time.
- MauranKilom 4y ago
  The quoted sentence is talking specifically about atomic variables. I would edit it if I still could.
samatman 4y ago
It's not that it's suspect, it's that equivalent Rust code will not compile. This is one of the things the borrow checker does, if something is atomic, you can't access it non-atomically, and this is assured at compile time. The 'borrow checker up in arms' is the same thing as 'the type checker up in arms because I'm treating an integer like a string'.
- MauranKilom 4y ago
  My point is that you can still have a race condition/logic bug, even if all your atomics are accessed atomically and all your borrows are fine (i.e. no data races). Note that I specifically wrote "[code] that assumes atomicVariable is true", not "code that accesses a shared resource under the assumptions that it has unique ownership because atomicVariable is true". Yes, this situation is much harder to produce by accident in rust - the language significantly raises the amount of things that are encoded/checked at compile-time and strongly guides you to safer designs. But I fail to see the "the equivalent Rust code will not compile" part. Here is a pretty stupid example including exactly the form of my original snippet: https://godbolt.org/z/6e18K85hT https://godbolt.org/z/6e18K85hT - You might get 2 or 3 printed after "see?". Or you might not get the first print at all (unlikely). And if you say "well nobody would write code like that" then that's exactly the point: It looks suspicious (even though it compiles).

josephcsible 4y ago

> Rust does not encode the difference between "is true" and "was, at least briefly, true" in the type system. Couldn't it encode that by taking advantage of the fact that nobody else can change a variable while you have it mutably borrowed?

marcosdumay 4y ago
Isn't that exactly what people do. This thread seems surreal to me. Rust type system does encode exactly what the later comments are complaining that isn't encoded. And you sate what code cares about the variable keeping its value through a code block, between a pair of braces.
- MauranKilom 4y ago
  What I meant was *For atomics*, rust does not encode the difference between "is true" and "was, at least briefly, true" in the type system. Obviously, rust has many ways to track this kind of distinction in a compile-time manner (and yes, the borrow checker is one of them). That was not in question.
  - marcosdumay 4y ago
    Hum, ok. You don't consider the borrow checker to be part of the type system. Well, it's perfectly fine to disagree on name definitions, but that is some fuzzy and dizzy line. Lifetimes impose themselves together with the static types features all the time.
MauranKilom 4y ago
The quoted sentence is talking specifically about atomic variables. I would edit it if I still could.

samatman 4y ago

It's not that it's suspect, it's that equivalent Rust code will not compile. This is one of the things the borrow checker does, if something is atomic, you can't access it non-atomically, and this is assured at compile time. The 'borrow checker up in arms' is the same thing as 'the type checker up in arms because I'm treating an integer like a string'.

MauranKilom 4y ago
My point is that you can still have a race condition/logic bug, even if all your atomics are accessed atomically and all your borrows are fine (i.e. no data races). Note that I specifically wrote "[code] that assumes atomicVariable is true", not "code that accesses a shared resource under the assumptions that it has unique ownership because atomicVariable is true". Yes, this situation is much harder to produce by accident in rust - the language significantly raises the amount of things that are encoded/checked at compile-time and strongly guides you to safer designs. But I fail to see the "the equivalent Rust code will not compile" part. Here is a pretty stupid example including exactly the form of my original snippet: https://godbolt.org/z/6e18K85hT https://godbolt.org/z/6e18K85hT - You might get 2 or 3 printed after "see?". Or you might not get the first print at all (unlikely). And if you say "well nobody would write code like that" then that's exactly the point: It looks suspicious (even though it compiles).