Remix.run Logo
▲ UncleMeat 2 hours ago

Would you say the same thing about Java? It’s type system is also unsound.

▲csande17 2 hours ago | parent | next [-]

I'm not an expert on the Java specification, but my understanding is that Java as a language is well-defined enough that we can say things like "Java's type system is unsound", independently from any specific implementation of Java.

You can't do that with Rust because "Rust's type system" is literally just the vague concept of "a type system that is safe". The implementation of this ideal in rustc can have flaws, but Rust itself cannot, because Rust itself has no flaws by definition.

▲mcherm 37 minutes ago | parent [-]

It is true that Rust does not have a complete formal specification for its type system which has been analyzed and proven to be sound.

You seem to be implying that because of this, Rust has no definition of its type system (other than whatever happens to be implemented in the current compiler). I would disagree.

As evidence, I would like to point out that not a single person argued that this flaw was not a bug, but was in fact the officially defined behavior. Clearly, the community has a shared understanding of what Rust's type system "ought" to do.

▲vrighter 2 hours ago | parent | prev [-]

but it isn't claiming to be saving you from things it can't prove it can either.