3 ms·

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 go

by 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
    To be fair though, almost every language is unsound in that metric. In fact, only an implementation that is verified and translated from a formal specification with the verifier and translator also similarly verified (ad infinitum) would be sound. Even PL researchers are not that strict---many academic papers don't actually prove the whole soundness, because the proof process is more or less automatic for the vast majority of cases to who know enough PL theories. (I can't say it's "mechanical", since the reasoning is still required. But the reasoning itself is not too involved for intended audiences.) Just like that not every security vulnerability is equally fatal, not every soundness bug is equally fatal. I reckon about three levels of severity: inherent to the design itself, not inherent to the design but reasonably user-visible, and pathological. As pcwalton pointed out, miri does show that this particular soundness bug is NOT inherent to the language design, and I believe that's true for most of 84 unsound bugs (please let me know any counter-example though, I haven't fully checked them). It remains to be seen whether there exist soundness bugs that are still user-visible enough.
    - jart 3y ago
      But languages like C / C++ don't claim to be safe.
      - lifthrasiir 3y ago
        Even Rust doesn't claim to be "safe" without a qualifier. From the website: > Rust’s rich type system and ownership model guarantee memory-safety and thread-safety — enabling you to eliminate many classes of bugs at compile-time. Note that it explicitly mentions "memory" safety and "thread" safety, which has a specific but reasonable definition in Rust (for example, memory safety doesn't cover physical memory leak). Also it explicitly mentions which portion of Rust is responsible for such guarantees, namely "type system" and "ownership model", and it is reasonably claimed that the ideal implementation of both will indeed completely achieve such guarantees. To be clear, the current implementation is also very close to that ideal to make such claim meaningful, but there is always a difference between the ideal and the practice.

by 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
  To be fair though, almost every language is unsound in that metric. In fact, only an implementation that is verified and translated from a formal specification with the verifier and translator also similarly verified (ad infinitum) would be sound. Even PL researchers are not that strict---many academic papers don't actually prove the whole soundness, because the proof process is more or less automatic for the vast majority of cases to who know enough PL theories. (I can't say it's "mechanical", since the reasoning is still required. But the reasoning itself is not too involved for intended audiences.) Just like that not every security vulnerability is equally fatal, not every soundness bug is equally fatal. I reckon about three levels of severity: inherent to the design itself, not inherent to the design but reasonably user-visible, and pathological. As pcwalton pointed out, miri does show that this particular soundness bug is NOT inherent to the language design, and I believe that's true for most of 84 unsound bugs (please let me know any counter-example though, I haven't fully checked them). It remains to be seen whether there exist soundness bugs that are still user-visible enough.
  - jart 3y ago
    But languages like C / C++ don't claim to be safe.
    - lifthrasiir 3y ago
      Even Rust doesn't claim to be "safe" without a qualifier. From the website: > Rust’s rich type system and ownership model guarantee memory-safety and thread-safety — enabling you to eliminate many classes of bugs at compile-time. Note that it explicitly mentions "memory" safety and "thread" safety, which has a specific but reasonable definition in Rust (for example, memory safety doesn't cover physical memory leak). Also it explicitly mentions which portion of Rust is responsible for such guarantees, namely "type system" and "ownership model", and it is reasonably claimed that the ideal implementation of both will indeed completely achieve such guarantees. To be clear, the current implementation is also very close to that ideal to make such claim meaningful, but there is always a difference between the ideal and the practice.