Dude, I'm a grad student in categorical logic and I've worked with PLT. That's why I used them as an example. To formalize most math, the simply typed lambda ca

Dude, I'm a grad student in categorical logic and I've worked with PLT. That's why I used them as an example. To formalize most math, the simply typed lambda calculus won't do, you need dependent types. But the logic used in math is almost always extensional, and type checking an extensional type theory isn't computable. Huge chunks of math, from analysis to chaos theory, are simply not computable.