I don't understand this reasoning at all. You have some form of contracts, whether you specify them or not. If it's too messy to formalize, that's still going to be an issue when you're working on it in an untyped language. At best you're just sweeping all those ugly edge cases under the rug.

>Also, what stops something like

having a more precise specification. E.g. adding a commutativity requirement would eliminate your example.