4 ms·

The rust borrow checker is under-specified (for a good reason). Can forsee lots of incompatible with two implementation

yjftsjthsd-h 4y ago
What good reason would there be for under-specifying it, that would create problems? Like, I can see wanting to leave flexibility in the implementation, but then different implementations should be fine if they both match what spec there is. The only problem would be if one implementation is more strict than it "admits" to being (in its written spec), which is a problem anyways.
- kelnos 4y ago
  I think there are two things that could be specified here: 1. What the borrow checker protects against, and what constitutes valid code. 2. What the borrow checker can actually prove is valid code. #2 tends to be much less than #1, because the compiler can only be so smart, and if it can't prove something correct (even if it might be correct), it takes the safe route and refuses to compile the code. #1 is probably pretty well specified, or at least wouldn't be hard to write down if someone really wanted to. #2 is a moving target, because the borrow checker in rustc gets smarter with some releases, and compiles code that it used to reject (because it's been taught to understand that code better and can prove it correct). So it's a lot harder to specify exactly what kinds of code the borrow checker will accept and reject. I could easily see a situation where gcc-rust claims to support all the language and stdlib features that a particular version of rustc supports, but has subtle differences in borrow checker behavior that causes it to reject some code that rustc accepts (or accept some code that rustc rejects). The behavior isn't incorrect, per se, but it would be frustrating for developers. It's also possible there could be similar issues with lifetime analysis.
kelnos 4y ago
Yeah, this would worry me too. It feels like the rustc policy on this is just to make the compiler smarter and smarter so it can accept more code that's actually valid (but couldn't prove was the case in previous versions). That's a great goal, but that makes it really hard to nail down what is and isn't allowed in a particular version of Rust. And if we assume that gcc Rust will always be playing catch-up to rustc, they will probably have a hard time enumerating rustc's borrow checker's behavior precisely enough to be able to replicate its behavior exactly in gcc Rust. So that means some code that rustc is ok with, gcc Rust might not be, and vice versa (even though all the code might be fine).
pornel 4y ago
It won't be. They plan to use the exact same code! Rust is designed to compile fine without any borrow checking (it reduces it to the C level of safety, but valid programs generate valid code). GCC will compile itself without a borrow checker. Then it will compile the existing borrow checker written in Rust, and then recompile itself with borrow checking.
- ByteJockey 4y ago
  > They plan to use the exact same code! Did they announce a change of plans? Their website just says that they have no plans for a borrow checker (i.e. it's not required to actually implement rust). From the website for the project: > There are no immediate plans for a borrow checker as this is not required to compile rust code and is the last pass in the RustC compiler. This can be handled as a separate project when we get to that point. Link here: https://rust-gcc.github.io/ https://rust-gcc.github.io/
  - ArrayBoundCheck 4y ago
    - pornel 4y ago
      If my information was inaccurate or out of date, you could have corrected me. I find your antagonizing cheer hurtful, and such a mean comment is unhelpful. Please be kinder.
      - ArrayBoundCheck 4y ago
  - pornel 4y ago
    The "separate project" you mention is integration of Polonius: https://lwn.net/Articles/871283/ https://lwn.net/Articles/871283/
kibwen 4y ago
The Rust type system wonks are highly motivated to precisely specify the entire type system, including the borrow checker. A new Types Team was formed earlier this year with the goal of producing a specification against which new type system features can be prototyped for soundness before being approved (borne out of, among other things, frustration with the long-unstable and long-incomplete "specialization" feature, which nobody has yet found a sound formulation for).

What good reason would there be for under-specifying it, that would create problems? Like, I can see wanting to leave flexibility in the implementation, but then different implementations should be fine if they both match what spec there is. The only problem would be if one implementation is more strict than it "admits" to being (in its written spec), which is a problem anyways.

kelnos 4y ago
I think there are two things that could be specified here: 1. What the borrow checker protects against, and what constitutes valid code. 2. What the borrow checker can actually prove is valid code. #2 tends to be much less than #1, because the compiler can only be so smart, and if it can't prove something correct (even if it might be correct), it takes the safe route and refuses to compile the code. #1 is probably pretty well specified, or at least wouldn't be hard to write down if someone really wanted to. #2 is a moving target, because the borrow checker in rustc gets smarter with some releases, and compiles code that it used to reject (because it's been taught to understand that code better and can prove it correct). So it's a lot harder to specify exactly what kinds of code the borrow checker will accept and reject. I could easily see a situation where gcc-rust claims to support all the language and stdlib features that a particular version of rustc supports, but has subtle differences in borrow checker behavior that causes it to reject some code that rustc accepts (or accept some code that rustc rejects). The behavior isn't incorrect, per se, but it would be frustrating for developers. It's also possible there could be similar issues with lifetime analysis.

kelnos 4y ago

Yeah, this would worry me too. It feels like the rustc policy on this is just to make the compiler smarter and smarter so it can accept more code that's actually valid (but couldn't prove was the case in previous versions). That's a great goal, but that makes it really hard to nail down what is and isn't allowed in a particular version of Rust. And if we assume that gcc Rust will always be playing catch-up to rustc, they will probably have a hard time enumerating rustc's borrow checker's behavior precisely enough to be able to replicate its behavior exactly in gcc Rust. So that means some code that rustc is ok with, gcc Rust might not be, and vice versa (even though all the code might be fine).

pornel 4y ago

It won't be. They plan to use the exact same code! Rust is designed to compile fine without any borrow checking (it reduces it to the C level of safety, but valid programs generate valid code). GCC will compile itself without a borrow checker. Then it will compile the existing borrow checker written in Rust, and then recompile itself with borrow checking.

ByteJockey 4y ago
> They plan to use the exact same code! Did they announce a change of plans? Their website just says that they have no plans for a borrow checker (i.e. it's not required to actually implement rust). From the website for the project: > There are no immediate plans for a borrow checker as this is not required to compile rust code and is the last pass in the RustC compiler. This can be handled as a separate project when we get to that point. Link here: https://rust-gcc.github.io/ https://rust-gcc.github.io/
- ArrayBoundCheck 4y ago
  - pornel 4y ago
    If my information was inaccurate or out of date, you could have corrected me. I find your antagonizing cheer hurtful, and such a mean comment is unhelpful. Please be kinder.
    - ArrayBoundCheck 4y ago
- pornel 4y ago
  The "separate project" you mention is integration of Polonius: https://lwn.net/Articles/871283/ https://lwn.net/Articles/871283/

kibwen 4y ago

The Rust type system wonks are highly motivated to precisely specify the entire type system, including the borrow checker. A new Types Team was formed earlier this year with the goal of producing a specification against which new type system features can be prototyped for soundness before being approved (borne out of, among other things, frustration with the long-unstable and long-incomplete "specialization" feature, which nobody has yet found a sound formulation for).