That's not what I mean. It's trivial to encode your types in such a way that it incorrectly implements domain logic and there is no meta-meta language enforcing correctness there.
That's not what I mean. It's trivial to encode your types in such a way that it incorrectly implements domain logic and there is no meta-meta language enforcing correctness there.
How so? To the extent that you use your types with your code, getting your types wrong will lead to either type errors in correct code (in which case you notice and fix them) or overly loose types that will allow incorrect code to pass (in which case you don't get an actual bug unless you make a corresponding mistake in your code).