[jcranmer]

That's someone who's defining "mental model" as effectively "build a formal model of how this things worth without actually using formalism for everything." Of course everyone in that thread is coming up with very complicated stuff, because OP explicitly asked them to do so.

Yes, Rust's borrower checker is more complicated than equivalent features in other languages. If you read the writings of the Rust language developers, you'll notice that they basically admit that it's where Rust sinks its entire complexity budget, so there's no room to spend it anywhere else. But I don't think it's too complex--it's not complex enough for average developers to not be productive. I would contrast this with C++'s template metaprogramming, which I believe to be too complex for average developers to be productive (e.g., trying to write templates that switch based on the types of the parameters, especially before if constexpr).