3 ms·
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
by b_e_n_t_o_n 1y ago
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.
- lmm 1y agoHow 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).