The problem is that we don’t have a sound, correct model. What we have is a compiler that seems pretty decent, but rejects some things that shouldn’t really be rejected, and accepts a few things that are iffy and potentially unsound. It’s a whole lot of code crafted in a comparatively ad hoc manner, whereas a true, correct model is likely to be simpler and more beautiful. Any specification would therefore be specifying the wrong thing, essentially a form of overfitting.
Suppose you’re a cave man and you’re just figuring out how to double numbers. So far, you’ve figured out how to double each number from 0 to 100. Someone asks you to write down your fancy rule so they can do something with it. Do you really want to be teaching everyone that the way to double a number is: “if the number is zero, the answer is zero; if one, then two, 2 ⇒ 4, 3 ⇒ 6, 4 ⇒ 8, &c. ad tedium”? Even if it covers all the required cases without error, it’s a mess. It’ll do for the moment for your own personal use, but you don’t want to be teaching it to other people until you figure out that you can say “to double a number, add the number to itself”.
Until we have a sound model, any attempt at specifying Rust would, for these key areas, be simply importing the current implementation of the compiler. That’s not a good sort of a specification.
Suppose you’re a cave man and you’re just figuring out how to double numbers. So far, you’ve figured out how to double each number from 0 to 100. Someone asks you to write down your fancy rule so they can do something with it. Do you really want to be teaching everyone that the way to double a number is: “if the number is zero, the answer is zero; if one, then two, 2 ⇒ 4, 3 ⇒ 6, 4 ⇒ 8, &c. ad tedium”? Even if it covers all the required cases without error, it’s a mess. It’ll do for the moment for your own personal use, but you don’t want to be teaching it to other people until you figure out that you can say “to double a number, add the number to itself”.
Until we have a sound model, any attempt at specifying Rust would, for these key areas, be simply importing the current implementation of the compiler. That’s not a good sort of a specification.