[movpasd]

If you push all your code into the type system, you're basically just writing your program in a clunkier, less readable language. So, you will just end up having to debug your type system, which defeats the whole purpose. I think expressive type systems are great, but like most things in engineering, it's a trade-off; the complexity of having to manually manage invariants vs. the complexity of managing the type system.

[xmcqdpt2]

The correct balance depends on how critical the piece of code you are working on is, and how much you want to write unit tests for it.

In cases where the type system can encode the invariants you care about, it can be worth the extra complexity so that you have code that has compiler enforced correctness (at least in some aspects). Of course, you can't do this for any invariant in a given type system (eg lifetimes are not representable in Java). When it is possible though, debugging a type system has the advantage that it's done on your local machine, away from prod.

[madsbuch]

> If you push all your code into the type system, you're basically just writing your program in a clunkier, less readable language.

It would be funny to see web servers running the typescript compiler (type checker) instead of a JS runtime, though.