Unexpected productivity boost of Rust

The example that the article gives relies on the borrow checker, which is not part of the usual Standard ML type system.

It is called affine type system, and there are ML descendents with it.

You can even go more crazy with linear types, effects, formal proofs or dependent types.

What Rust has achieved, was definitely make these ideas more mainstream.

Can the type system catch such things across translation unit boundaries? I know this is a big limit of C like compilers without whole program compilation.

Ultimately the answer is just "Yes". You know how an array of six integers is a different type from an array of three integers even though they're both arrays of integers ? If you're unclear on that it's worth a moment to go refresh, if your only experience is in C it's a deep dive - no trouble it's valuable knowledge.

In Rust lifetimes for references are part of the type, so &'a str and &'b str could be different types, even though they're both string slice references.

Beyond that, Rust tracks two important "thread safety" properties called Sync and Send, and so if your Thing ends up needing to be Send (because another thread gets given this type) but it's not Send, that's a type error just as surely as if it lacked some other needed property needed for whatever you do with the Thing, like it's not totally ordered (Ord) or it can't be turned into an iterator (IntoIterator)