Yeah, but the problem is that programming languages and compilers change all the time, making it hard to maintain a formal model of them. Exceptions exist (CompCert C and WebAssembly are two good examples) but for example, the semantics of raw pointers in Rust are intentionally under-defined because the compiler writers want to keep changing it.

Rust is still young, so it's taking the opportunity to thoroughly explore its options. As it grows older, it will solidify its decisions, even if it means committing to something that will be broken in the future. I look forward to the day that it becomes legacy (with all love)!