With the rise of powerful programmable computers, and the development of programming languages for same, type theory has found practical application in the development of programming language type systems. Definitions of "type system" in the context of programming languages vary, but the following definition due to Benjamin C. Pierce roughly corresponds to the current consensus in the type theory community:
"hello" + 5would be illegal. Hence, any program permitted by the type system would be provably free from the erroneous behavior of adding strings and numbers.
The design and implementation of type systems is a topic nearly as broad as the topic of programming languages itself. In fact, type theory proponents commonly proclaim that the design of type systems is the very essence of programming language design: "Design the type system correctly, and the language will design itself."
Note that type theory, as described herein, refers to static typing disciplines. Programming systems and languages that employ dynamic typing do not prove the absence of any program behavior; they merely raise an error at runtime, when the program attempts to execute this behavior. Some claim that "dynamic typing" is a misnomer for this reason. In any case, the two should not be confused.
Note: Static type systems vs. dynamic types
Major historical developments
Practical impact of type theory
Connections to constructive logic
Other topics we may want to add here
External links: