[joshspankit]

> Beware though, often human intuition can be contradictory. This means that a formalization of our intuitive notions of type correctness will also be contradictory and therefore unusable.

It is my very strong suspicion that in almost all (if not all) of the similar cases in programming methodology, there have been not just arguments on both sides, but implementations and real-world lessons on both sides.

A veeeery minor example: I’m equally as sure that someone designed and deployed systems that specifically created errors when you tried to pass less than the required number of params as I am that other people (or even the same people) specifically designed and implemented systems where params were optional (most likely because they hated having to specify empty params every time).