There is a connection between type theory and logic, where types are propositions, and type checking performs the role of checking whether a proof of a proposition is correct (Curry-Howard isomorphism).
But I can imagine a different connection: There seems to be a similarity between type checking and checking whether a particular mathematical structure satisfies a set of axioms.
We might say that propositions (axioms) are formalized as types (just as in the CH-isomorphism), but that now, an instance of a proposition (i.e. an instance of that type) is not a proof of the proposition, but a model of it. Type checking then takes the role of checking whether a particular mathematical structure is indeed a model of that axiom.
Is there a formalization of "checking whether a structure is a model of a proposition" as type checking? Could you explain such a formalization, or point to an explanation of it?