In 1979 Martin-Löf wrote the paper “Constructive Mathematics and Computer Programming” where he explained that intuitionistic type theory is a programming language which can also be used as a formal foundation for constructive mathematics. Shortly after that, interactive proof systems which help the user to derive valid judgments in the theory, so called proof assistants, were developed.