3 ms·

> This can't possibly be guaranteed to work just by disabling the checker, can it? It works in the sense that the borrow checker stops bothering you and the co

by masklinn 10mo ago

> This can't possibly be guaranteed to work just by disabling the checker, can it? It works in the sense that the borrow checker stops bothering you and the compiler will compile your code. It will even work fine as long as you don't write code which invokes UB (which does include code which would not pass the borrow checker, as the borrow checker necessarily rejects valid programs in order to forbid all invalid programs).

dataflow 10mo ago
> It will even work fine as long as you don't write code which invokes UB (which does include code which would not pass the borrow checker, as the borrow checker necessarily rejects valid programs in order to forbid all invalid programs). To be clear, by "this" I meant "[allowing] code that would normally violate Rust's borrowing rules to compile and run successfully," which both of us seem to believe to be UB.
- masklinn 10mo ago
  Not quite, there is code which fails borrow checking but is safe and sound. That is part of why a number of people have been waiting for Polonius and / or the tree borrows model, most classic are relatively trivial cases of "check then update" which fail to borrow check but are obviously non-problematic e.g. pub fn get_or_insert ( map: &'_ mut HashMap<u32, String>, ) -> &'_ String { if let Some(v) = map.get(&22) { return v; } map.insert(22, String::from("hi")); &map[&22] } Though ultimately even if either or both efforts bear fruits they will still reject programs which are well formed: that is the halting problem, a compiler can either reject all invalid programs or accept all valid programs, but it can not do both, and the former is generally considered more valuable, so in order to reject all invalid programs compilers will necessarily reject some valid programs.
  - hyghjiyhu 10mo ago
    Imo if you run into the halting problem it's because you are trying to do too much. In particular I think what you actually want is to check soundness based on the "shape" of the code rather than the reason about which variables can have which values and what that means for soundness. flag=false; if flag { use_after_free(); } can be rejected with a clear conscience.
  - dataflow 10mo ago
    I don't feel you're quite following what I'm saying unfortunately. In your specific example: couldn't the optimizer just optimize out all the mutations you've written, under the assumption that such a program would not have passed borrow-checking and thus isn't a case it needs to handle? Wouldn't this make it so that if you disabled borrow checking, you would get incorrect codegen vs. what you intended? This seems like an entirely legal and sane optimization; I'm not sure how you're assuming something like this outside the realm of possibility. You seem to be operating on some (generous) underlying assumptions about what a borrow-checker-violating Rust program really means and what optimizations the compiler has the liberty to make even when borrow-checker assumptions are violated. But are you sure that assumption is well-founded? What is it formally based on?
    - masklinn 10mo ago
      > I don't feel you're quite following what I'm saying unfortunately. Disagreeing with your plainly incorrect assertion is not "not following" what you're saying. > In your specific example: couldn't the optimizer just optimize out all the mutations you've written, under the assumption that such a program would not have passed borrow-checking and thus isn't a case it needs to handle? No. The borrow checker ensures specific rules are followed, the borrow checker is not the rules themselves, and the optimisations are based on the underlying rules not on the borrow checker. The program above abides by the underlying rules, it's literally the sort of examples used by people working on the next generation borrow checker, but the current borrow checker is not able to understand that. > This seems like an entirely legal and sane optimization It's neither of those things. > You seem to be operating on some (generous) underlying assumptions about what a borrow-checker-violating Rust program really means and what optimizations the compiler has the liberty to make even when borrow-checker assumptions are violated. But are you sure that assumption is well-founded? What is it formally based on? They are not assumptions, or generous. They are an understanding of the gap between the capabilities of the NLL borrow checker and "Behavior considered undefined". They are what anyone working on the borrow checker sees as limitations of the borrow checker (some fixable, others intrinsic).
      - dataflow 10mo ago
  - TruePath 10mo ago
    That gets a bit tricky in terms of what you mean by valid programs. I presume what you mean is that you can't write a compiler that accepts every function which always returns the borrowed reference and reject every piece of code which fails to do so. Though it's technically a bit different than the halting problem as this issue remains even if you assume that the function terminates -- you only want to show that the reference is returned assuming the code terminates if it isn't returned because it enters an infinite loop that's not a leak.

dataflow 10mo ago

> It will even work fine as long as you don't write code which invokes UB (which does include code which would not pass the borrow checker, as the borrow checker necessarily rejects valid programs in order to forbid all invalid programs). To be clear, by "this" I meant "[allowing] code that would normally violate Rust's borrowing rules to compile and run successfully," which both of us seem to believe to be UB.

masklinn 10mo ago
Not quite, there is code which fails borrow checking but is safe and sound. That is part of why a number of people have been waiting for Polonius and / or the tree borrows model, most classic are relatively trivial cases of "check then update" which fail to borrow check but are obviously non-problematic e.g. pub fn get_or_insert ( map: &'_ mut HashMap<u32, String>, ) -> &'_ String { if let Some(v) = map.get(&22) { return v; } map.insert(22, String::from("hi")); &map[&22] } Though ultimately even if either or both efforts bear fruits they will still reject programs which are well formed: that is the halting problem, a compiler can either reject all invalid programs or accept all valid programs, but it can not do both, and the former is generally considered more valuable, so in order to reject all invalid programs compilers will necessarily reject some valid programs.
- hyghjiyhu 10mo ago
  Imo if you run into the halting problem it's because you are trying to do too much. In particular I think what you actually want is to check soundness based on the "shape" of the code rather than the reason about which variables can have which values and what that means for soundness. flag=false; if flag { use_after_free(); } can be rejected with a clear conscience.
- dataflow 10mo ago
  I don't feel you're quite following what I'm saying unfortunately. In your specific example: couldn't the optimizer just optimize out all the mutations you've written, under the assumption that such a program would not have passed borrow-checking and thus isn't a case it needs to handle? Wouldn't this make it so that if you disabled borrow checking, you would get incorrect codegen vs. what you intended? This seems like an entirely legal and sane optimization; I'm not sure how you're assuming something like this outside the realm of possibility. You seem to be operating on some (generous) underlying assumptions about what a borrow-checker-violating Rust program really means and what optimizations the compiler has the liberty to make even when borrow-checker assumptions are violated. But are you sure that assumption is well-founded? What is it formally based on?
  - masklinn 10mo ago
    > I don't feel you're quite following what I'm saying unfortunately. Disagreeing with your plainly incorrect assertion is not "not following" what you're saying. > In your specific example: couldn't the optimizer just optimize out all the mutations you've written, under the assumption that such a program would not have passed borrow-checking and thus isn't a case it needs to handle? No. The borrow checker ensures specific rules are followed, the borrow checker is not the rules themselves, and the optimisations are based on the underlying rules not on the borrow checker. The program above abides by the underlying rules, it's literally the sort of examples used by people working on the next generation borrow checker, but the current borrow checker is not able to understand that. > This seems like an entirely legal and sane optimization It's neither of those things. > You seem to be operating on some (generous) underlying assumptions about what a borrow-checker-violating Rust program really means and what optimizations the compiler has the liberty to make even when borrow-checker assumptions are violated. But are you sure that assumption is well-founded? What is it formally based on? They are not assumptions, or generous. They are an understanding of the gap between the capabilities of the NLL borrow checker and "Behavior considered undefined". They are what anyone working on the borrow checker sees as limitations of the borrow checker (some fixable, others intrinsic).
    - dataflow 10mo ago
- TruePath 10mo ago
  That gets a bit tricky in terms of what you mean by valid programs. I presume what you mean is that you can't write a compiler that accepts every function which always returns the borrowed reference and reject every piece of code which fails to do so. Though it's technically a bit different than the halting problem as this issue remains even if you assume that the function terminates -- you only want to show that the reference is returned assuming the code terminates if it isn't returned because it enters an infinite loop that's not a leak.