> how do you express, not in Rust source code but in the English language, all the checks to be performed, and neither miss things out nor unknowingly accept programs a real Rust compiler will reject ?
I think this is unintentionally stuck in the mindset of "the purpose of a language specification document is to enable armchair language lawyers to flame each other on Usenet about whether or not such-and-such degenerate edge case is technically valid". But a specification doesn't need to be written in English, it can be written as a formal proof, and indeed I would expect a theoretical Rust spec to specify the behavior of the borrow checker as just such a proof. Rust's borrow checking may no longer be as simple as the lexically-scoped model that existed as of Rust 1.0, but it's not like the extensions that have been added since then are ad-hoc; they're all still designed to result in a model that is provably sound.
I think this is unintentionally stuck in the mindset of "the purpose of a language specification document is to enable armchair language lawyers to flame each other on Usenet about whether or not such-and-such degenerate edge case is technically valid". But a specification doesn't need to be written in English, it can be written as a formal proof, and indeed I would expect a theoretical Rust spec to specify the behavior of the borrow checker as just such a proof. Rust's borrow checking may no longer be as simple as the lexically-scoped model that existed as of Rust 1.0, but it's not like the extensions that have been added since then are ad-hoc; they're all still designed to result in a model that is provably sound.