I think this is an interesting doc, but the argument that global properties can be guaranteed by a type system is false, so there will trivially be counterexamp

I think this is an interesting doc, but the argument that global properties can be guaranteed by a type system is false, so there will trivially be counterexamples of type systems. In fact, for any extensional type theory, we have the interesting result that type inhabitation is undecideable. Further, when looking at intersection types, there's also a theory saying they're undecideable, and many more edge cases which I can't remember. So the result is that we have a lot of "patching" in compilers or runtimes that try to fill some of these holes, but that's to be expected.