Type systems can do some pretty miraculous things. For example, you could distinguish between a connected and disconnected socket with types so that you don't a

Type systems can do some pretty miraculous things. For example, you could distinguish between a connected and disconnected socket with types so that you don't accidentally send on a disconnected socket. I guess I'm arguing both sides now. My point is that one needs to root out the weird cases somehow and that it's often hard to have "100%" validation of inputs. One's initial understanding of what is the valid and invalid state space is often incorrect.