> If I don't get the mathematically-sound safety net, why would I apply 1 type system to my code, let alone n? I don't it is intended to imply that extrisic ty

> If I don't get the mathematically-sound safety net, why would I apply 1 type system to my code, let alone n? I don't it is intended to imply that extrisic type systems wouldn't be sound. As for why you'd want several type systems, one benefit I imagine is that different type systems could verify different aspects of your program, instead of forcing to cram everything into one type system. Afaik just because type system is sound doesn't alone mean that it can be used practically to prove every interesting property of a program.