I'm not a type theory guy, but it seems like you could rank Rust's type system somewhere in the realm of ML, Ocaml, Haskell, COQ, Agda, ATS, or something else.

I'm not a type theory guy, but it seems like you could rank Rust's type system somewhere in the realm of ML, Ocaml, Haskell, COQ, Agda, ATS, or something else. If Rust uses more memory and computation than those, then it's reasonable to assume there is another reason. I'm guessing you could have a very efficient implementation of Rust, but that it would be rewrite instead of an incremental fix. This statement is likely to be unpopular.