The most important distinction in a language is

whether it has GC or not.

>>5
Rust's type system is based on multiple decades of research on linear logic and type theory. It's not been formally proven correct, in the same way that no full language has had a formal proof; only strict toy subsets.

IHBT.