4 ms·

As noted on that GitHub page, fixing the bug will become possible once rustc adopts a new trait solver: https://blog.rust-lang.org/inside-rust/2023/07/17/trait-

As noted on that GitHub page, fixing the bug will become possible once rustc adopts a new trait solver: https://blog.rust-lang.org/inside-rust/2023/07/17/trait-system-refactor-initiative.html https://blog.rust-lang.org/inside-rust/2023/07/17/trait-syst...

Maken 3y ago
Everything is always a new solver away.
- TylerE 3y ago
  a sufficiently advanced new solver. Just like how the lisp guys insisted for decades that a sufficiently advanced compiler would solve all their performance woes. Right up until it became obvious that it couldn't. Feels a bit like early chess engines. They tried to create super sophisticated heuristics to determine move quality, but then one person (or more probably multiple people independently more or less simultaneously) realized it's both easier and better to just do more or less the simplest thing that can possibly work, but do it as much as possible in the allotted time. In other words - don't try to logically decide on the best move with some super advanced set of rules. Just assign a fairly basic and straightforward score based on calculating every reasonble move out 15, 20, 30 moves deep.
  - Georgelemental 3y ago
    In the case of the trait solver, there is a clear end goal to reach: "the type system should be sound." This is a yes/no question, which you can prove/disprove mathematically. (I suppose chess engines also have an end goal of perfect play, but that is a much harder problem)
    - dzaima 3y ago
      There's a very simple solver that completes that goal: one that reports that it cannot prove any code as correct. So there must be a secondary goal of "maximize the amount of accepted code", which is a significantly less trivial question.
      - TylerE 3y ago
        Yes, exactly. Saying "just do the thing correctly, duh!" is easy. Ya know the saying about the difference between theory and practice?
      - Georgelemental 3y ago
        I guess you have to add an implied "and preserves backward compatibility for (>99.9% of) sound code that compiles today" condition
    - wbl 3y ago
      A sound type system has strong limits on expressiveness, and even stronger if you want type inference to work. It's very easy to start tripping over those limits as you add features, as users of some Haskell extensions can attest.
  - agalunar 3y ago
    This is beside the point, but the only way an engine can possibly search to depth 20 is by being extremely selective, using heuristics to guess move quality (such as static exchange analysis, the killer move heuristic, history tables, countermove tables, follow-up tables, late move reductions, &c). The discovery was that it's often better to guess move quality dynamically, based on the observed utility of similar moves in similar contexts, rather than statically. But this is not especially "simple", and it still (necessarily!) involves judging up front a few moves as likely-good and the vast majority of moves as unworthy of further examination. Both type A engines (to use Shannon's terminology) and type B engines are relatively weak. The strong engines are all hybrids.
meindnoch 3y ago
Is it going to be even slower than the current one?
- dralley 3y ago
  Who says the current one is slow? Just because the compiler as a whole isn't the fastest one around doesn't mean the responsibility falls equally on every constituant part of the compiler.
  - estebank 3y ago
    The most obvious slow down people perceive of compile times is due to monomorphization. It is a combinational explosion when instantiating every generic type that is in use, and it exacerbates the issue of rustc producing verbose LLVM IR bytecode.
nialv7 3y ago
Can you quote the relevant part? Because IIUC lifetime checks have nothing to do with the trait solver. There's a new borrow checker however, but that's not going to fix this either
- anderskaseorg 3y ago
  https://github.com/rust-lang/rust/issues/25860#issuecomment-1455898550 https://github.com/rust-lang/rust/issues/25860#issuecomment-... “Similarly, the reason why niko's approach is not yet implemented is simply that getting the type system to a point where we even can implement this is Hard. Fixing this bug is blocked on replacing the existing trait solver(s): #107374. A clean fix for this issue (and the ability to even consider using proof objects), will then also be blocked blocked on coinductive trait goals and explicit well formed bounds. We should then be able to add implications to the trait solver. So I guess the status is that we're slowly getting there but it is very hard, especially as we have to be incredibly careful to not break backwards compatibility.” https://blog.rust-lang.org/inside-rust/2023/07/17/trait-system-refactor-initiative.html https://blog.rust-lang.org/inside-rust/2023/07/17/trait-syst... “The new trait solver implementation should also unblock many future changes, most notably around implied bounds and coinduction. For example, it will allow us to remove many of the current restrictions on GATs and to fix many long-standing unsound issues, like #25860. Some unsound issues will already be fixed at the point of stabilization while others will require additional work afterwards.”
  - jart 3y ago
    > unsound issues Apparently there's 84 open issues which the Rust developers consider unsound issues. https://github.com/rust-lang/rust/issues?q=is%3Aissue+is%3Aopen+label%3AI-unsound+ https://github.com/rust-lang/rust/issues?q=is%3Aissue+is%3Ao... That's it. Rust's claims are over and done with. How can it be safe if it's unsound? By the principle of noncontradiction and the laws of thought itself, let no one speak that word anymore. You can call Rust memory safer, but until those bugs get fixed, it's wrong to call it safe.
    - lifthrasiir 3y ago

Maken 3y ago

Everything is always a new solver away.

TylerE 3y ago
a sufficiently advanced new solver. Just like how the lisp guys insisted for decades that a sufficiently advanced compiler would solve all their performance woes. Right up until it became obvious that it couldn't. Feels a bit like early chess engines. They tried to create super sophisticated heuristics to determine move quality, but then one person (or more probably multiple people independently more or less simultaneously) realized it's both easier and better to just do more or less the simplest thing that can possibly work, but do it as much as possible in the allotted time. In other words - don't try to logically decide on the best move with some super advanced set of rules. Just assign a fairly basic and straightforward score based on calculating every reasonble move out 15, 20, 30 moves deep.
- Georgelemental 3y ago
  In the case of the trait solver, there is a clear end goal to reach: "the type system should be sound." This is a yes/no question, which you can prove/disprove mathematically. (I suppose chess engines also have an end goal of perfect play, but that is a much harder problem)
  - dzaima 3y ago
    There's a very simple solver that completes that goal: one that reports that it cannot prove any code as correct. So there must be a secondary goal of "maximize the amount of accepted code", which is a significantly less trivial question.
    - TylerE 3y ago
      Yes, exactly. Saying "just do the thing correctly, duh!" is easy. Ya know the saying about the difference between theory and practice?
    - Georgelemental 3y ago
      I guess you have to add an implied "and preserves backward compatibility for (>99.9% of) sound code that compiles today" condition
  - wbl 3y ago
    A sound type system has strong limits on expressiveness, and even stronger if you want type inference to work. It's very easy to start tripping over those limits as you add features, as users of some Haskell extensions can attest.
- agalunar 3y ago
  This is beside the point, but the only way an engine can possibly search to depth 20 is by being extremely selective, using heuristics to guess move quality (such as static exchange analysis, the killer move heuristic, history tables, countermove tables, follow-up tables, late move reductions, &c). The discovery was that it's often better to guess move quality dynamically, based on the observed utility of similar moves in similar contexts, rather than statically. But this is not especially "simple", and it still (necessarily!) involves judging up front a few moves as likely-good and the vast majority of moves as unworthy of further examination. Both type A engines (to use Shannon's terminology) and type B engines are relatively weak. The strong engines are all hybrids.

meindnoch 3y ago

Is it going to be even slower than the current one?

dralley 3y ago
Who says the current one is slow? Just because the compiler as a whole isn't the fastest one around doesn't mean the responsibility falls equally on every constituant part of the compiler.
- estebank 3y ago
  The most obvious slow down people perceive of compile times is due to monomorphization. It is a combinational explosion when instantiating every generic type that is in use, and it exacerbates the issue of rustc producing verbose LLVM IR bytecode.

nialv7 3y ago

Can you quote the relevant part? Because IIUC lifetime checks have nothing to do with the trait solver. There's a new borrow checker however, but that's not going to fix this either

anderskaseorg 3y ago
https://github.com/rust-lang/rust/issues/25860#issuecomment-1455898550 https://github.com/rust-lang/rust/issues/25860#issuecomment-... “Similarly, the reason why niko's approach is not yet implemented is simply that getting the type system to a point where we even can implement this is Hard. Fixing this bug is blocked on replacing the existing trait solver(s): #107374. A clean fix for this issue (and the ability to even consider using proof objects), will then also be blocked blocked on coinductive trait goals and explicit well formed bounds. We should then be able to add implications to the trait solver. So I guess the status is that we're slowly getting there but it is very hard, especially as we have to be incredibly careful to not break backwards compatibility.” https://blog.rust-lang.org/inside-rust/2023/07/17/trait-system-refactor-initiative.html https://blog.rust-lang.org/inside-rust/2023/07/17/trait-syst... “The new trait solver implementation should also unblock many future changes, most notably around implied bounds and coinduction. For example, it will allow us to remove many of the current restrictions on GATs and to fix many long-standing unsound issues, like #25860. Some unsound issues will already be fixed at the point of stabilization while others will require additional work afterwards.”
- jart 3y ago
  > unsound issues Apparently there's 84 open issues which the Rust developers consider unsound issues. https://github.com/rust-lang/rust/issues?q=is%3Aissue+is%3Aopen+label%3AI-unsound+ https://github.com/rust-lang/rust/issues?q=is%3Aissue+is%3Ao... That's it. Rust's claims are over and done with. How can it be safe if it's unsound? By the principle of noncontradiction and the laws of thought itself, let no one speak that word anymore. You can call Rust memory safer, but until those bugs get fixed, it's wrong to call it safe.
  - lifthrasiir 3y ago