> but even current official sources like https://rust-lang.org/ say things like "Rust’s rich type system and ownership model guarantee memory-safety" that are only true of the vague-ideal "Rust language" and are not true of the type system they actually designed and implemented in the Rust compiler.

That's an understandable point, though I think something similar would arguably still apply even if Rust had a "proper" spec since a "proper" spec doesn't necessarily rule out underspecification/omissions/mistakes/etc, both in the spec and in the implementation. A "real" formal spec à la WebAssembly might solve that issue, but given the lack of time/resources for a "normal" spec at the time a "real" one would have been a pipe dream at best.

That being said, I think it's an interesting question as to what should be done if/when you discover an issue like the trait coherence one, whether you have a spec or not. "Aspirational" marketing doesn't exactly feel nice, but changing your marketing every time you discover/fix a bug also doesn't exactly feel nice for other reasons.

Bit of a fun fact - it appears that the particular trait coherence issue actually has existed in some form since Rust 1.0, and was only noticed a few years later when the issue was filed. Perhaps a proper specification effort would have caught it (especially since one of the devs said they had concerns when implementing a relevant check), but given it had taken that long to discover I wouldn't be too surprised if it would have been missed anyway.