Earlier quoted context omitted.
Well, I'm familiar with model theory and Church's simple theory of types, but I don't think things like that are useful in practice. Perhaps the concept of currying would be an exception, if I were a Haskell programmer.
I am not sure that you have really understood the topics you have named. All high-level programming languages give you a set of fundamental types and the ability to construct user-defined types. Currying is not an exception but falls under the same model if one considers it as a Relation between "sets of functions". Also by Curry-Howard correspondence you have "formula/proposition = type" and "proof = function". So y…
At the risk of nitpicking:
Certainly it's a benefit to structure and understand code such that you can reason about it effectively, but prove goes too far. Almost no real code is proven correct, the ergonomics of formal methods are still far too poor for that.