While making constructive mathematics rigorous was Martin-Löfs original goal, he was quite early aware of the applications to computer science. See for instance

While making constructive mathematics rigorous was Martin-Löfs original goal, he was quite early aware of the applications to computer science. See for instance his 1979ish paper «Constructive Mathematics and Computer Programming»[0] [0]: 1982 version: https://raw.githubusercontent.com/michaelt/martin-lof/master/pdfs/Constructive-mathematics-and-computer-programming-1982.pdf https://raw.githubusercontent.com/michaelt/martin-lof/master...