4 ms·

> The truth is that the borrow checker is not perfect. The borrow checker prevents you from doing dangerous things and it does that. However it often feels too

> The truth is that the borrow checker is not perfect. The borrow checker prevents you from doing dangerous things and it does that. However it often feels too restrictive. In my experience though the borrow checker actually is wrong much less often than you think it is and just requires you to think a bit differently. I would love to see this explored in more detail. The borrow checker is, from what I can tell, one of the most important and novel parts of Rust. I'd love to see more detailed examples of where: 1. it kept you from doing something idiomatic that you knew was safe but you just couldn't convince the borrow checker of it. 2. it kept you from doing something that seemed safe, but then you realized that it was actually telling you something important. Also: > Even if it would turn out that the borrow checker is not sound Wait, is this an actual risk? Is there some lingering doubt that the borrow checker is actually sound?

mcpherrinm 12y ago
Soundness bugs come up once in a while, so yeah there is doubts. I wouldn't claim it to be sound until there is at least a proof of soundness of a theoretical model of it (which you can then show the implementation matches)
- haberman 12y ago
  That's a little scary. But giving it solid theoretical justification sounds like a perfect thesis for some CS or math grad student.
  - dbaupp 12y ago
    https://github.com/nikomatsakis/rust-redex https://github.com/nikomatsakis/rust-redex is a theoretical model of the interesting part of Rust (by one of the core-developers). I don't think it's complete though.
  - bjz_ 12y ago
    There is actually a CS student working on it... from the University of Washington I think? Check out rust-redex. I don't know what the status is though - it doesn't seem to have been updated in a while. Anyway the devs have said that whilst a 1.0 release will mean backwards compatibility for language features, they will fix any soundness bugs that come to light.
steveklabnik 12y ago
Currently, borrows are always lexical. It'd be nice to have non-lexical borrows. It's on the todo list.
- haberman 12y ago
  Interesting. What is an example of a non-lexical borrow that could potentially be proven safe?
  - dbaupp 12y ago
    Searching[1] a data-structure (like a hashmap) will return a borrowed reference to that data, which "freezes" the hashmap while the borrow exists. And, due to lexical borrowing, it is frozen even if there was nothing (that is, if the return value was `None` which contains no references linked to the original map). The following is currently illegal because the `insert` is trying to modify the borrowed map. match some_map.find(&a_key) { Some(x) => println!("reference to value {}", x), None => { println!("not found, inserting instead"); some_map.insert(a_key, some_value); } } #6393 is the relevant issue. [1]: http://doc.rust-lang.org/nightly/std/collections/struct.HashMap.html#method.find http://doc.rust-lang.org/nightly/std/collections/struct.Hash... [6393]: https://github.com/rust-lang/rust/issues/6393 https://github.com/rust-lang/rust/issues/6393
    - Ygg2 12y ago
      How exactly does one decide if scope is lexical or non-lexical? Or more precisely how do you tell compiler?
      - steveklabnik 12y ago
        There is a Drop trait that has one method, drop(). It's like a destructor. It's called for you, but you can also call it yourself. fn foo(x: &something) { // stuff x.drop(); // more stuff, } // if we didn't drop, x gets drop()-ped here If we had non-lexical borrows, after we drop x, we could have it be un-borrowed. currently, x is still considered borrowed until the end of foo(). This is sort of a contrived example, but if you check out the ticket it has better ones. There's also good examples here: http://www.reddit.com/r/rust/comments/2hy06n/a_fresh_look_at_rust_armin_ronachers_thoughts_and/ckxdh5w http://www.reddit.com/r/rust/comments/2hy06n/a_fresh_look_at...
kibwen 12y ago
> it kept you from doing something that seemed safe, but > then you realized that it was actually telling you > something important. One of the reasons that I know Rust is on to something is how often I've seen this scenario occur on IRC. It's great to watch someone come in with a complaint about appeasing the borrow checker, only to later realize that what they were attempting to do was actually subtly unsafe. For the former point about things that the borrow checker doesn't have enough information to allow, see http://www.reddit.com/r/rust/comments/279yw3/borrowing_from_an_array_need_help/ http://www.reddit.com/r/rust/comments/279yw3/borrowing_from_... for an example.
- aidenn0 12y ago
  It's also really a pain now to get the borrow checker to be happy with boxed structures now that box isn't implemented in the compiler. You need to first borrow the whole structure, and then things within it.

mcpherrinm 12y ago

Soundness bugs come up once in a while, so yeah there is doubts. I wouldn't claim it to be sound until there is at least a proof of soundness of a theoretical model of it (which you can then show the implementation matches)

haberman 12y ago
That's a little scary. But giving it solid theoretical justification sounds like a perfect thesis for some CS or math grad student.
- dbaupp 12y ago
  https://github.com/nikomatsakis/rust-redex https://github.com/nikomatsakis/rust-redex is a theoretical model of the interesting part of Rust (by one of the core-developers). I don't think it's complete though.
- bjz_ 12y ago
  There is actually a CS student working on it... from the University of Washington I think? Check out rust-redex. I don't know what the status is though - it doesn't seem to have been updated in a while. Anyway the devs have said that whilst a 1.0 release will mean backwards compatibility for language features, they will fix any soundness bugs that come to light.

steveklabnik 12y ago

Currently, borrows are always lexical. It'd be nice to have non-lexical borrows. It's on the todo list.

haberman 12y ago
Interesting. What is an example of a non-lexical borrow that could potentially be proven safe?
- dbaupp 12y ago
  Searching[1] a data-structure (like a hashmap) will return a borrowed reference to that data, which "freezes" the hashmap while the borrow exists. And, due to lexical borrowing, it is frozen even if there was nothing (that is, if the return value was `None` which contains no references linked to the original map). The following is currently illegal because the `insert` is trying to modify the borrowed map. match some_map.find(&a_key) { Some(x) => println!("reference to value {}", x), None => { println!("not found, inserting instead"); some_map.insert(a_key, some_value); } } #6393 is the relevant issue. [1]: http://doc.rust-lang.org/nightly/std/collections/struct.HashMap.html#method.find http://doc.rust-lang.org/nightly/std/collections/struct.Hash... [6393]: https://github.com/rust-lang/rust/issues/6393 https://github.com/rust-lang/rust/issues/6393
  - Ygg2 12y ago
    How exactly does one decide if scope is lexical or non-lexical? Or more precisely how do you tell compiler?
    - steveklabnik 12y ago
      There is a Drop trait that has one method, drop(). It's like a destructor. It's called for you, but you can also call it yourself. fn foo(x: &something) { // stuff x.drop(); // more stuff, } // if we didn't drop, x gets drop()-ped here If we had non-lexical borrows, after we drop x, we could have it be un-borrowed. currently, x is still considered borrowed until the end of foo(). This is sort of a contrived example, but if you check out the ticket it has better ones. There's also good examples here: http://www.reddit.com/r/rust/comments/2hy06n/a_fresh_look_at_rust_armin_ronachers_thoughts_and/ckxdh5w http://www.reddit.com/r/rust/comments/2hy06n/a_fresh_look_at...

kibwen 12y ago

> it kept you from doing something that seemed safe, but > then you realized that it was actually telling you > something important. One of the reasons that I know Rust is on to something is how often I've seen this scenario occur on IRC. It's great to watch someone come in with a complaint about appeasing the borrow checker, only to later realize that what they were attempting to do was actually subtly unsafe. For the former point about things that the borrow checker doesn't have enough information to allow, see http://www.reddit.com/r/rust/comments/279yw3/borrowing_from_an_array_need_help/ http://www.reddit.com/r/rust/comments/279yw3/borrowing_from_... for an example.

aidenn0 12y ago
It's also really a pain now to get the borrow checker to be happy with boxed structures now that box isn't implemented in the compiler. You need to first borrow the whole structure, and then things within it.