Types in Programming Languages, Between Modelling, Abstraction, and Correctness

The notion of type to designate a class of values, and the operations on those values, is a central feature of any modern programming language. In fact, we keep calling them programming languages, but the part of a modern language devoted to the actual specification of the control flow (that is, programming stricto sensu) is only a fraction of the language itself, and two different languages are not much apart under that perspective. What “makes a language” are much more its modelling capabilities to describe complex relations between portions of code and between data. In a word, the central part of a language is made by the abstraction mechanisms it provides to model its application domain(s), all issues the language theorist may well group together in the type chapter of a language definition.