Types have always been a hard sell for me. I honestly never have issues with types being wrong when I write code, and I understand that this is missing the point. The point is that the types define a very concrete interface and we know up front when the interfaces break, and can statically check that the interface is correct everywhere.

I feel that mathematical types are so far distant from the type system of something like C or C++ that the term foot guns itself somewhat.