We're not using "type theory" the same way, I think. I'm thinking in terms of - simply typed lambda calculus - System F - dependent type theory (ML

We're not using "type theory" the same way, I think. I'm thinking in terms of - simply typed lambda calculus - System F - dependent type theory (MLTT) - linear types - row types - and so on But it's subtle to talk about. It's not like there is a single type theory that underlies Typescript or Rust, either. These practical languages have partial, (and somewhat post-hoc) formalizations of their systems.