5 ms·

the Rust compiler is able to infer that allowing two mutable borrows is safe as long as one of them is never used This (i.e. proving a variable is never u

the Rust compiler is able to infer that allowing two mutable borrows is safe as long as one of them is never used This (i.e. proving a variable is never used) is impossible in general since it is equivalent to the halting problem. There are many cases where it can be solved, so the compiler lets the programmer get away with this in the cases where one of the mutable borrows is provably not used. Now imagine re-factoring the code so that the compiler could no longer produce the proof. Now an error is generated and the programmer is left scratching their head wondering where this new error came from.

nh23423fefe 3y ago
why is it a head scratcher? the error message seems clear?
- waynecochran 3y ago
  The head scratcher is that as soon as the compiler can't produce the proof (even though the borrow still may be unreachable) an error is generated. The programmer will be wondering why a new error cropped up when they may not have been doing anything that was semantically any different.
parentheses 3y ago
compiler != runtime ultimately no code is free of side effects. this is a tool to mark code as safe and propagate that safety up the call stack to make your code's safety something you can reason about. it's definitely true that if a piece of code is unsafe, you need to be more careful. (not a rust programmer, but have had to fight the compiler when i first looked at it)
- waynecochran 3y ago
  This is a static error. A compiler generated error. With static analysis reachability is not computable.
Rusky 3y ago
The compiler doesn't do anything here that is hard to understand- its approximate solution works purely in terms of the control flow graph, so there is a very clear and bright dividing line between "you have a use of this variable here" and not, which is never impacted by anything subtle about the values of conditions or whatever. The closest to head-scratching that I have ever seen here are the sorts of errors that include "note: value may be accessed in another iteration of this loop," or perhaps the corner cases that Polonius aims to solve if you count those.
layer8 3y ago
In an ideal (?) world, a refactoring would come along with a machine proof that the refactored code is equivalent to the original code (because otherwise, how can you be sure?). In that case, the compiler would also be able to prove that the code is still safe. I believe that type checking should closely match the reasoning programmers do in their head, and thereby verify the correctness of that reasoning. Conversely, this means that programmers must express their reasoning through the type system. If something doesn’t typecheck, either the reasoning as expressed is wrong or incomplete, or the programmer has used some reasoning that cannot be expressed in the type system (meaning that the type system is lacking in that respect).
- waynecochran 3y ago
  Proving that two programs are the same is not decidable either.
  - scarmig 3y ago
    Proving that two real numbers are the same is not decidable either. Despite that, there are some real numbers that we can prove are equal to each other (rarely).
  - quickthrower2 3y ago
    “You can’t do it in general” is the bathwater.
    - waynecochran 3y ago
      Yeah I am not clever enough to come up with a baby worth throwing out. Restricted to lexical scope seems pretty reasonable. Maybe someday this will compile: let mut viridian = Colour(52, 161, 128); let x = &mut viridian; let y = &mut viridian; if find_counter_example_to_Reimann_Hypothesis { do something with x and y }
      - pyrale 3y ago
        More like you're arguing that there is no baby in the bath you want to throw out. Coming back to your previous comment: > This (i.e. proving a variable is never used) is impossible in general since it is equivalent to the halting problem. Many useful provers/programs don't suffer from the halting problem. Just because you're given a turing machine doesn't mean you can't use a subset of it with different properties.
Hugsun 3y ago
The quote betrays a slight misunderstanding of non lexical lifetimes. The two borrows happen in separate implicit scopes. The first borrow is only valid until the second borrow is made. At that point it's dropped. So the two mutable references can't exist at the same time. A refactor that breaks this ordering results in code that obviously shouldn't work in the eyes of any non-beginner rust programmer.
- legerdemain 3y ago
  You can 100% have multiple mutable references to the same variable in the same scope, without the first one getting dropped. For example: fn main() { let mut s = String::from("s"); let mut1: &mut _ = &mut s; let mut2: &mut _ = &mut *mut1; *mut2 = String::from("t"); println!("using mut2: {mut2}"); println!("using mut1: {mut1}"); } Some people use a mental model of reference lifetimes that allows "discontinuous lifetimes" where the valid region has holes. I don't think that's how the compiler models reborrowing, and even under that model, `mut1` is created before `mut2` and gets dropped after `mut2`.
  - jayshua 3y ago
    I read this as mut1 and mut2 both being downgraded to shared references because they aren't used to mutate anymore. I'd imagine that's not what's actually happening though?
    - vlovich123 3y ago
      No - that they are both &mut _ indicates that a mutable reference is being acquired regardless of whether or not they’re used for any mutation. Possibly the compiler could automatically lower to a shared reference if it detects no mutation access locally but there may be design reasons why that’s impossible (+ you can’t have a mutable and a shared reference simultaneously anyway so downgrading to shared would still be disallowed)
  - saghm 3y ago
    > and even under that model, `mut1` is created before `mut2` and gets dropped after `mut2` I think what you're calling "holes" are what I'd just consider to be "lazy" borrowing, where the reference doesn't really matter until the first time it's dereferenced. The only use of mut1 that happens before the end of mut2's lifetime is to assign a reference mut2 to a value that is never used. In other words, mut1 is never actually dereferenced while mut2 exists. I don't consider `&mut *` as dereferencing because it's just syntax for saying "make a new mutable reference to the same thing", which is necessary because mutable references don't implement Copy or Clone. If you instead used `let mut2 = &mut s;`, it would be abundantly clear; they don't really overlap in any way that matters because nothing would change if mut1 didn't exist at all until after mut2 no longer needed to.
lmm 3y ago
Yeah. This is why I think NLL is a mistake, just as I've come to think that implicit TCE is a mistake. Our tools must not only be correct but also comprehensible.
- throwaway17_17 3y ago
  Do you mean Tail Call Elimination? If so, are you thinking of all tail calls, or are you more focusing on the conversion of recursive calls to iteration?
  - lmm 3y ago
    Yes, tail call elimination. Conversion of recursion to iteration is the most common case, I don't really understand what you're asking by distinguishing between "all tail calls" and "the conversion of recursive calls to iteration". The point is it's a similar case where a seemingly innocuous refactor can break your program because the implicit TCE stops working.
    - throwaway17_17 3y ago
      Regarding the distinguishing between recursive tail calls and other tail calls: The conversion of tail calls to direct jumps seems to me a simpler conversion, where refactoring would be less likely to introduce errors. The conversion of recursive calls to iteration is different, I can see how the implicit conversion could lead to much more sensitive preconditions that refactoring could cause to not be satisfied. My initial (and rather lazily considered) reaction to the potential for breakage could be wrong, I doubt it would be worth an exhaustive testing effort to validate. I find TCE to be a conversion that is worth the potential downsides in heavily functional paradigms, but I certainly sympathize with becoming more skeptical of implicit alterations to code as written.
      - lmm 3y ago
        > The conversion of tail calls to direct jumps seems to me a simpler conversion, where refactoring would be less likely to introduce errors. The conversion of recursive calls to iteration is different, I can see how the implicit conversion could lead to much more sensitive preconditions that refactoring could cause to not be satisfied. Isn't it the same thing? If you convert a tail call to a jump, if the place you jumped to leads back to the same line (directly or indirectly) then you've converted recursion to iteration. Iteration is ultimately implemented as jumps too. > I doubt it would be worth an exhaustive testing effort to validate. I find TCE to be a conversion that is worth the potential downsides in heavily functional paradigms, but I certainly sympathize with becoming more skeptical of implicit alterations to code as written. I've been bitten by it often enough to be wary. I swear I once saw a language that had an explicit keyword for tail calls (not just an annotation to error out if TCO wasn't performed, but a keyword to make a tail call and no implicit optimization), which sounded like the best solution, but I can't find it now.
SkiFire13 3y ago
The statement "proving a variable is never used" is not fully specified. What does it mean for it to not be used? (Or rather, not be used again?). One way to interpret it (which I think is the one you used) is that at runtime it will no longer be read/wrote. Another one is to that it is no longer syntactically referenced, which is much easier to reason about and statically prove.

nh23423fefe 3y ago

why is it a head scratcher? the error message seems clear?

waynecochran 3y ago
The head scratcher is that as soon as the compiler can't produce the proof (even though the borrow still may be unreachable) an error is generated. The programmer will be wondering why a new error cropped up when they may not have been doing anything that was semantically any different.

parentheses 3y ago

compiler != runtime ultimately no code is free of side effects. this is a tool to mark code as safe and propagate that safety up the call stack to make your code's safety something you can reason about. it's definitely true that if a piece of code is unsafe, you need to be more careful. (not a rust programmer, but have had to fight the compiler when i first looked at it)

waynecochran 3y ago
This is a static error. A compiler generated error. With static analysis reachability is not computable.

Rusky 3y ago

The compiler doesn't do anything here that is hard to understand- its approximate solution works purely in terms of the control flow graph, so there is a very clear and bright dividing line between "you have a use of this variable here" and not, which is never impacted by anything subtle about the values of conditions or whatever. The closest to head-scratching that I have ever seen here are the sorts of errors that include "note: value may be accessed in another iteration of this loop," or perhaps the corner cases that Polonius aims to solve if you count those.

layer8 3y ago

In an ideal (?) world, a refactoring would come along with a machine proof that the refactored code is equivalent to the original code (because otherwise, how can you be sure?). In that case, the compiler would also be able to prove that the code is still safe. I believe that type checking should closely match the reasoning programmers do in their head, and thereby verify the correctness of that reasoning. Conversely, this means that programmers must express their reasoning through the type system. If something doesn’t typecheck, either the reasoning as expressed is wrong or incomplete, or the programmer has used some reasoning that cannot be expressed in the type system (meaning that the type system is lacking in that respect).

waynecochran 3y ago
Proving that two programs are the same is not decidable either.
- scarmig 3y ago
  Proving that two real numbers are the same is not decidable either. Despite that, there are some real numbers that we can prove are equal to each other (rarely).
- quickthrower2 3y ago
  “You can’t do it in general” is the bathwater.
  - waynecochran 3y ago
    Yeah I am not clever enough to come up with a baby worth throwing out. Restricted to lexical scope seems pretty reasonable. Maybe someday this will compile: let mut viridian = Colour(52, 161, 128); let x = &mut viridian; let y = &mut viridian; if find_counter_example_to_Reimann_Hypothesis { do something with x and y }
    - pyrale 3y ago
      More like you're arguing that there is no baby in the bath you want to throw out. Coming back to your previous comment: > This (i.e. proving a variable is never used) is impossible in general since it is equivalent to the halting problem. Many useful provers/programs don't suffer from the halting problem. Just because you're given a turing machine doesn't mean you can't use a subset of it with different properties.

Hugsun 3y ago

The quote betrays a slight misunderstanding of non lexical lifetimes. The two borrows happen in separate implicit scopes. The first borrow is only valid until the second borrow is made. At that point it's dropped. So the two mutable references can't exist at the same time. A refactor that breaks this ordering results in code that obviously shouldn't work in the eyes of any non-beginner rust programmer.

legerdemain 3y ago
You can 100% have multiple mutable references to the same variable in the same scope, without the first one getting dropped. For example: fn main() { let mut s = String::from("s"); let mut1: &mut _ = &mut s; let mut2: &mut _ = &mut *mut1; *mut2 = String::from("t"); println!("using mut2: {mut2}"); println!("using mut1: {mut1}"); } Some people use a mental model of reference lifetimes that allows "discontinuous lifetimes" where the valid region has holes. I don't think that's how the compiler models reborrowing, and even under that model, `mut1` is created before `mut2` and gets dropped after `mut2`.
- jayshua 3y ago
  I read this as mut1 and mut2 both being downgraded to shared references because they aren't used to mutate anymore. I'd imagine that's not what's actually happening though?
  - vlovich123 3y ago
    No - that they are both &mut _ indicates that a mutable reference is being acquired regardless of whether or not they’re used for any mutation. Possibly the compiler could automatically lower to a shared reference if it detects no mutation access locally but there may be design reasons why that’s impossible (+ you can’t have a mutable and a shared reference simultaneously anyway so downgrading to shared would still be disallowed)
- saghm 3y ago
  > and even under that model, `mut1` is created before `mut2` and gets dropped after `mut2` I think what you're calling "holes" are what I'd just consider to be "lazy" borrowing, where the reference doesn't really matter until the first time it's dereferenced. The only use of mut1 that happens before the end of mut2's lifetime is to assign a reference mut2 to a value that is never used. In other words, mut1 is never actually dereferenced while mut2 exists. I don't consider `&mut *` as dereferencing because it's just syntax for saying "make a new mutable reference to the same thing", which is necessary because mutable references don't implement Copy or Clone. If you instead used `let mut2 = &mut s;`, it would be abundantly clear; they don't really overlap in any way that matters because nothing would change if mut1 didn't exist at all until after mut2 no longer needed to.

lmm 3y ago

Yeah. This is why I think NLL is a mistake, just as I've come to think that implicit TCE is a mistake. Our tools must not only be correct but also comprehensible.

throwaway17_17 3y ago
Do you mean Tail Call Elimination? If so, are you thinking of all tail calls, or are you more focusing on the conversion of recursive calls to iteration?
- lmm 3y ago
  Yes, tail call elimination. Conversion of recursion to iteration is the most common case, I don't really understand what you're asking by distinguishing between "all tail calls" and "the conversion of recursive calls to iteration". The point is it's a similar case where a seemingly innocuous refactor can break your program because the implicit TCE stops working.
  - throwaway17_17 3y ago
    Regarding the distinguishing between recursive tail calls and other tail calls: The conversion of tail calls to direct jumps seems to me a simpler conversion, where refactoring would be less likely to introduce errors. The conversion of recursive calls to iteration is different, I can see how the implicit conversion could lead to much more sensitive preconditions that refactoring could cause to not be satisfied. My initial (and rather lazily considered) reaction to the potential for breakage could be wrong, I doubt it would be worth an exhaustive testing effort to validate. I find TCE to be a conversion that is worth the potential downsides in heavily functional paradigms, but I certainly sympathize with becoming more skeptical of implicit alterations to code as written.
    - lmm 3y ago
      > The conversion of tail calls to direct jumps seems to me a simpler conversion, where refactoring would be less likely to introduce errors. The conversion of recursive calls to iteration is different, I can see how the implicit conversion could lead to much more sensitive preconditions that refactoring could cause to not be satisfied. Isn't it the same thing? If you convert a tail call to a jump, if the place you jumped to leads back to the same line (directly or indirectly) then you've converted recursion to iteration. Iteration is ultimately implemented as jumps too. > I doubt it would be worth an exhaustive testing effort to validate. I find TCE to be a conversion that is worth the potential downsides in heavily functional paradigms, but I certainly sympathize with becoming more skeptical of implicit alterations to code as written. I've been bitten by it often enough to be wary. I swear I once saw a language that had an explicit keyword for tail calls (not just an annotation to error out if TCO wasn't performed, but a keyword to make a tail call and no implicit optimization), which sounded like the best solution, but I can't find it now.

SkiFire13 3y ago

The statement "proving a variable is never used" is not fully specified. What does it mean for it to not be used? (Or rather, not be used again?). One way to interpret it (which I think is the one you used) is that at runtime it will no longer be read/wrote. Another one is to that it is no longer syntactically referenced, which is much easier to reason about and statically prove.