A type system was actually the original solution to Russell's paradox [1]. Today, we have type theories such as Martin-Löf type theory and Homotopy type theory, which can be used as a basis for constructive mathematics (i.e. mathematics, where law of the excluded middle, ∀(p : Proposition).p ∨ ¬p, doesn't generally hold — more or less).
