A type system is a tractable syntactic method for proving the absense of certain program behaviours by classifying phrases according to the kinds of values they compute
Types systems were first formalised in the 1900’s as a way of avoiding logical paradoxes in mathematics.
Sidenote: Bertrand Russels paradox is to do with the definition of naive set theory. Naive set theory states that any definable collection is a set. the Contradiction arises when you define the set R to be the set of all sets that are not members of themselves. If R is not a member of itself, then it must contain itself, by definition, and if it contains itself, then it doesn’t match its own definition
R = { x | x ∉ x }, then R ∈ R ⟺ R ∉ R
Type systems are conservative, they can prove the absence of some bad behaviour but cannot prove their presence, and hence must sometimes reject programs that behave well at run time