Types have been widely used in programming for a long time. Early high-level programming languages introduced types of integers and floating point numbers. Modern programming languages often have rich type systems with many constructs for forming new types. Intuitionistic type theory is a functional programming language where the type system is so rich that practically any conceivable property of a program can be expressed as a type. Types can thus be used as specifications of the task of a program.