The notion of proof of a proposition is of the most fundamental notions in Martin-Löf's work on philosophical logic, since it is conceptually prior to the notion of truth - cf "Truth of a proposition, evidence of a judgement, validity of a proof" (p.414). But, as far as I know, he never really gave an explicit philosophical explanation of it.
So what is a proof of a proposition for Martin-Löf? Generally speaking, we can put the question as
- What is a term of a type for Martin-Löf?
(given the Curry-Howard or proposition-as-types correspondence.)