If your type system can handle the case where I can divert code flow along an unsandboxed path by replacing functions from the system libraries even before you can achieve code execution (and long before you certainly though I had code execution), I would like to hear it. But expressed in a less brusque way: yes, encoding state in your type system is generally great, and there is a lot of work being done in languages where you can formally “prove” guarantees about your code. The issue is that your proofs only hold true if the system they run on is correct, you chose exactly the right thing to check, you didn’t just leave out part of the program because you couldn’t fit it into the type system…it’s a nontrivial problem.