> almost all type systems in wide use today are extremely dumb compared to an actual human This isn't really true in the specific sense though (obviously it's

> almost all type systems in wide use today are extremely dumb compared to an actual human This isn't really true in the specific sense though (obviously it's inherently true in the general sense, but that's less relevant here). Type systems are true & accurate representations of data structure and usage - any given actual human (a) may have an inaccurate mental representation of that at any given time, (b) that mental representation may change over time, (c) that mental representation will almost always be incomplete for any reasonably complex system. Being "dumb" or intelligent isn't about representing data structures in memory, but the particular problem being discussed here is very much about that: in that context, humans are usually "dumber" than type systems.