Type systems of programming languages have become rather powerful and complex. Thus they became a research area of their own.
Constructive type theory has its origins in both programming languages and constructive mathematics. The Curry-Howard correspondence shows that certain formal systems can be viewed both as functional programming languages with powerful type systems and as constructive logic. On the one hand this gives new insight into the two formerly separate areas and on the other hand systems have been developed which unite a specification language with a programming language and thus enable the computer-assisted derivation of a program from a specification in a single system.