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.
replyYou 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!
replyI mean yes, part of our understanding of systems is a social one!
replySure, but in Rust's case the social understanding is "there exists some type system that guarantees perfect memory safety, and has the general aesthetic features associated with rustc's type system, and 'Rust' is defined to be whatever that type system ends up being".
replyThis is a nice ideal, but it doesn't actually exist in concrete terms as a design. It can never have flaws because the definition of it is just "rustc without all the flaws".
Haskell is in a similar boat with regards to a missing formal spec.
replyThere is some work on that: https://www.youtube.com/watch?v=qk_P8piUclI
reply