[black_knight]

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...