[ggreg84]

> 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]

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]

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.

[nialv7]

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?

[layer8]

It’s a consequence of not having a formal and formally-proved type system.