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.
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.
Eh. Java was released in 1995. Smashing the Stack for Fun and Profit was published in 1996. The big selling point for java in the beginning was write-once-run-everywhere. Being a GCed language was also a selling point, but that is distinct from memory safety as a selling point.
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.
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.
The true specification was inside our hearts all along!
4 replies →
but it isn't claiming to be saving you from things it can't prove it can either.
Memory safety was always a major selling point for java.
Eh. Java was released in 1995. Smashing the Stack for Fun and Profit was published in 1996. The big selling point for java in the beginning was write-once-run-everywhere. Being a GCed language was also a selling point, but that is distinct from memory safety as a selling point.