4 ms·

My biggest concern with Rust is the sloppiness around the distinction between a "compiler bug" and a "hole in the type system." This is more of a specification

My biggest concern with Rust is the sloppiness around the distinction between a "compiler bug" and a "hole in the type system." This is more of a specification bug even though Rust doesn't have a formal specification: the problem is the design of the language itself, not that a Rust programmer wrote the wrong thing in the source code: https://counterexamples.org/nearly-universal.html?highlight=Rust#nearly-universal-quantification https://counterexamples.org/nearly-universal.html?highlight=...

ggreg84 3y ago
> My biggest concern with Rust is the sloppiness around the distinction between a "compiler bug" and a "hole in the type system." That bug is marked as I-unsound, which means that it introduces a hole in the type system. And so are all other similar bugs, i.e., your concern seems to be unfounded, since you can actually click on the I-unsound label, and view all current bugs of this kind (and past closed ones as well!).
- nicklecompte 3y ago
  Perhaps I should have said "hole in the type theory" to clarify what I meant. To be clear I wasn't trying to imply the rustc maintainers were ignorant of the difference. I meant that Rust programmers seem to treat fundamental design flaws in the language as if they are temporary bugs in the compiler. (e.g. the comment I was responding to) There's a big difference between "this buggy program should not have compiled but somehow rustc missed it" and "this buggy program will compile because the Rust language has a design flaw."
  - pcwalton 3y ago
    But it's not a fundamental design flaw in the language, nor is it a "hole in the type theory". It's a compiler bug. The compiler isn't checking function contravariance properly. Miri catches the problem, while rustc doesn't.
    - nicklecompte 3y ago
      I believe it really is a flaw in the language, it's impossible for any compiler to check contravariance properly in this edge case. I don't think anything in this link is incorrect: https://counterexamples.org/nearly-universal.html?highlight=Rust#nearly-universal-quantification https://counterexamples.org/nearly-universal.html?highlight=... (and it seems the rustc types team endorses this analysis) I am not at all familiar with Miri. Does Miri consider a slightly different dialect of Rust where implicit constraints like this become explicit but inferred? Sort of like this proposal from the GH issue: https://github.com/rust-lang/rust/issues/25860#issuecomment-174011431 https://github.com/rust-lang/rust/issues/25860#issuecomment-... but the "where" clause is inferred at compile time. If so I wouldn't call that a "fix" so much as a partial mitigation, useful for static analysis but not actually a solution to the problem in rustc. I believe that inference problem is undecidable in general and that rustc would need to do something else.
      - anderskaseorg 3y ago
        In the language, fn foo<'a, 'b, T>(_: &'a &'b (), v: &'b T) -> &'a T { v } should be equivalent to fn foo<'a, 'b, T>(_: &'a &'b (), v: &'b T) -> &'a T where 'b: 'a { v } because the type &'a &'b is only well-formed if 'b: 'a. However, in the implementation, only the first form where the constraint is left implicit is subject to the bug: the implicit constraint is incorrectly lost when 'static is substituted for 'b. This is clearly an implementation bug, not a language bug (insofar as there is a distinction at all—ideally there would be a written formal specification that we could point to, but I don’t think there’s any disagreement in principle about what it should say about this issue).
        nicklecompte 3y ago
        See my other comment above: https://news.ycombinator.com/item?id=39448909 https://news.ycombinator.com/item?id=39448909 The point is that rustc does not even implicitly have the "where 'b: 'a { v }" clause. The programmer knows "where 'b: 'a { v }" is true because otherwise &'a &'b would be self-contradictory, and in most cases that's more than enough. But in certain edge cases this runs into problems with the contravariance requirement since we can substitute either one of the 'bs with a type that outlives 'b (i.e. 'static), and the design of contravariance lets us do this pretty arbitrarily.
  - nialv7 3y ago
    Why is this distinction important? It's still something you fix by changing what programs the compiler accepts or rejects. Or were you trying to imply this is unfixable?
    - chatmasta 3y ago
      The distinction matters because any existing code that breaks with the compiler fix was either relying on "undefined behavior" (in the case of a compiler bug incorrectly implementing the spec), so you can blame the user, or it was relying on "defined behavior" (in the case of a compiler bug correctly implementing a badly designed spec), so you can't blame the user. I suppose the end result is the same, but it might impact any justification around whether the fix should be a minor security patch or a major version bump and breaking update.
      - estebank 3y ago
        Rust's backwards compatibility assurances explicitly mention that breaking changes to fix unsoundness are allowed. In practice the project would be careful to avoid breaking more than strictly necessary for a fix. In the case of user code that isn't unsound but breaks with the changes to the compiler/language, that would be breaking backwards compatibility, in which case there might be a need to relegate the change to a new edition.
      - nialv7 3y ago
        Well first of all, Rust doesn't even have a spec. And I would also advocate for not blaming anyone, let's just fix this bug ;)
    - nicklecompte 3y ago
      Probably better to be maximally pedantic here: - Assume our language has a specification, even if it's entirely in your head - a "correct" program is a program that is 100% conformant to the specification - an "incorrect" program is a program which violates the specification in some way Let's say we have a compiler that compiles correct programs with 100% accuracy, but occasionally compiles incorrect programs instead of erroring out. If the language specification is fine but the compiler implementation has a bug, then fixing the compiler does not affect the compilation behavior of correct programs. (Unless of course you introduce a new implementation-level bug.) But if the language specification has a bug, then this does not hold: the specification has to change to fix the bug, and it is likely that at least some formerly correct programs would no longer obey this new specification. So this is true: > It's still something you fix by changing what programs the compiler accepts or rejects But in one case you are only changing what incorrect programs the compiler accepts, and in the other you are also changing the correct programs the compiler accepts. It's much more serious.
- layer8 3y ago
  It’s a consequence of not having a formal and formally-proved type system.

ggreg84 3y ago

> My biggest concern with Rust is the sloppiness around the distinction between a "compiler bug" and a "hole in the type system." That bug is marked as I-unsound, which means that it introduces a hole in the type system. And so are all other similar bugs, i.e., your concern seems to be unfounded, since you can actually click on the I-unsound label, and view all current bugs of this kind (and past closed ones as well!).

nicklecompte 3y ago
Perhaps I should have said "hole in the type theory" to clarify what I meant. To be clear I wasn't trying to imply the rustc maintainers were ignorant of the difference. I meant that Rust programmers seem to treat fundamental design flaws in the language as if they are temporary bugs in the compiler. (e.g. the comment I was responding to) There's a big difference between "this buggy program should not have compiled but somehow rustc missed it" and "this buggy program will compile because the Rust language has a design flaw."
- pcwalton 3y ago
  But it's not a fundamental design flaw in the language, nor is it a "hole in the type theory". It's a compiler bug. The compiler isn't checking function contravariance properly. Miri catches the problem, while rustc doesn't.
  - nicklecompte 3y ago
    I believe it really is a flaw in the language, it's impossible for any compiler to check contravariance properly in this edge case. I don't think anything in this link is incorrect: https://counterexamples.org/nearly-universal.html?highlight=Rust#nearly-universal-quantification https://counterexamples.org/nearly-universal.html?highlight=... (and it seems the rustc types team endorses this analysis) I am not at all familiar with Miri. Does Miri consider a slightly different dialect of Rust where implicit constraints like this become explicit but inferred? Sort of like this proposal from the GH issue: https://github.com/rust-lang/rust/issues/25860#issuecomment-174011431 https://github.com/rust-lang/rust/issues/25860#issuecomment-... but the "where" clause is inferred at compile time. If so I wouldn't call that a "fix" so much as a partial mitigation, useful for static analysis but not actually a solution to the problem in rustc. I believe that inference problem is undecidable in general and that rustc would need to do something else.
    - anderskaseorg 3y ago
      In the language, fn foo<'a, 'b, T>(_: &'a &'b (), v: &'b T) -> &'a T { v } should be equivalent to fn foo<'a, 'b, T>(_: &'a &'b (), v: &'b T) -> &'a T where 'b: 'a { v } because the type &'a &'b is only well-formed if 'b: 'a. However, in the implementation, only the first form where the constraint is left implicit is subject to the bug: the implicit constraint is incorrectly lost when 'static is substituted for 'b. This is clearly an implementation bug, not a language bug (insofar as there is a distinction at all—ideally there would be a written formal specification that we could point to, but I don’t think there’s any disagreement in principle about what it should say about this issue).
      - nicklecompte 3y ago
        See my other comment above: https://news.ycombinator.com/item?id=39448909 https://news.ycombinator.com/item?id=39448909 The point is that rustc does not even implicitly have the "where 'b: 'a { v }" clause. The programmer knows "where 'b: 'a { v }" is true because otherwise &'a &'b would be self-contradictory, and in most cases that's more than enough. But in certain edge cases this runs into problems with the contravariance requirement since we can substitute either one of the 'bs with a type that outlives 'b (i.e. 'static), and the design of contravariance lets us do this pretty arbitrarily.
- nialv7 3y ago
  Why is this distinction important? It's still something you fix by changing what programs the compiler accepts or rejects. Or were you trying to imply this is unfixable?
  - chatmasta 3y ago
    The distinction matters because any existing code that breaks with the compiler fix was either relying on "undefined behavior" (in the case of a compiler bug incorrectly implementing the spec), so you can blame the user, or it was relying on "defined behavior" (in the case of a compiler bug correctly implementing a badly designed spec), so you can't blame the user. I suppose the end result is the same, but it might impact any justification around whether the fix should be a minor security patch or a major version bump and breaking update.
    - estebank 3y ago
      Rust's backwards compatibility assurances explicitly mention that breaking changes to fix unsoundness are allowed. In practice the project would be careful to avoid breaking more than strictly necessary for a fix. In the case of user code that isn't unsound but breaks with the changes to the compiler/language, that would be breaking backwards compatibility, in which case there might be a need to relegate the change to a new edition.
    - nialv7 3y ago
      Well first of all, Rust doesn't even have a spec. And I would also advocate for not blaming anyone, let's just fix this bug ;)
  - nicklecompte 3y ago
    Probably better to be maximally pedantic here: - Assume our language has a specification, even if it's entirely in your head - a "correct" program is a program that is 100% conformant to the specification - an "incorrect" program is a program which violates the specification in some way Let's say we have a compiler that compiles correct programs with 100% accuracy, but occasionally compiles incorrect programs instead of erroring out. If the language specification is fine but the compiler implementation has a bug, then fixing the compiler does not affect the compilation behavior of correct programs. (Unless of course you introduce a new implementation-level bug.) But if the language specification has a bug, then this does not hold: the specification has to change to fix the bug, and it is likely that at least some formerly correct programs would no longer obey this new specification. So this is true: > It's still something you fix by changing what programs the compiler accepts or rejects But in one case you are only changing what incorrect programs the compiler accepts, and in the other you are also changing the correct programs the compiler accepts. It's much more serious.
layer8 3y ago
It’s a consequence of not having a formal and formally-proved type system.