Is that really true though? To me this sounds more like making the validation of the program an afterthought, at best. Even in very academic mathematical models

Is that really true though? To me this sounds more like making the validation of the program an afterthought, at best. Even in very academic mathematical models, introducing types early usually doesn't introduce much of a cognitive burden. I maintain that even when developers don't think that they're reasoning in terms of types, in many cases they are: "This is function 'x'. It takes two items of type 'T', which have to have a member 'a', which is a number. Function 'x' multiples the two 't.a' values together and returns a new 'T' with the result in its 'a' field." If you opted to forego static typing, every step of the above function would require you to validate that you're dealing with the types you think you are. This kind of example isn't even at all uncommon.