the negative and positive use of types (gating inputs vs. witnessing implementations) get confused when talking about programming languages. It seems to me the positive aspect is overwhelmingly where programmers find frustration.