The point about inter-procedural borrow checking is fair -- and in fact not a matter of "sufficiently smart" borrow checker, but a rather fundamental type system limitation. But the flaw here is pretty manageable -- sometimes you can get away with calling .split_at_mut(...), sometimes you can borrow the field directly instead of going through a wrapper method, sometimes you have to be mindful to provide a split_at_mut equivalent yourself. Last I checked there was some work being done on "partial borrows", which could solve this.

Most of the other criticisms are pretty disappointing, though.

> The following example is a famous illustration of how it can't properly reason across branches, either:

Except that function body would have been better rewritten as map.entry(key).or_default() -- which passes the borrow checker just fine and is more performant as it avoids multiple lookups. I suspect many other examples would benefit from being re-written into higher-level primitives that can be easier to borrow-check in this manner.

> But what's the point of the rules in this case, though? Here, the ownership rules does not prevent use after free, or double free, or data races, or any other bug. It's perfectly clear to a human that this code is fine and doesn't have any actual ownership issues.

What if Id represents a file descriptor that ought to be closed when the value ceases to exist? Or some other type of handle? This is an ownership problem: these are not limited to memory safety issues. For very good API stability reasons, without an explicit #[derive(Clone,Copy)] the compiler is not free to assume the type represents pure information that can be copied at will, but can only treat it as one potentially containing owned resources, that just happens not to include any at this time.

> References to temporary values, e.g. values created in a closure, are forbidden even though it's obvious to a human that the solution is simply to extend the lifetime of the value to its use outside the closure.

Which is to say, to what? The type signature does not say whether a closure will be called immediately or in another thread after two hours. And in which stack frame should the value be stored, the soon-to-be-exiting closure's?