Type Systems
Type Systems for Programming Language were invented by mathematicians before electronic computers were invented.
What is a type? A meaningful subset of the set of the domain of data values used in a program. Types are used to describe the intended behavior of program operations.
The concept is derived from mathematics. A functions has a specified domain set and a co-domain set which are often called types. In the terminology of types, a function with domain A and co-domain B has type A ? B. If a function is defined by a formula, the variables used in the formula typically have specified types.
Mathematicians informally check that uses of functions and variables in formulas are respected just as they informally check that reasoning used in proofs is sound.
In computer programs, some forms of “type checking” can be formalized and automated.