In intuitionistic mathematics, a proposition is true only when a proof of it has been experienced. Following the BHK semantics, a proof of A → B is an algorithm that, when given a proof of A, will yield a proof of B. So, with a proof of A → B and a proof of A, there is an obvious way to get a proof of B.
My question, though, is about when a proof of B is experienced. Is it enough to think of the algorithm, think of the proof of A, and juxtapose the two? Or do I have to actually compute the proof of B into a normal form? Note that the question is recursive: given that the proofs of A → B and A are themselves proofs, must we have normal forms of these to conclude anything meaningful?
I'm thinking of this in terms of Martin-Löf type theory. There, we might think of this as a distinction between lazy evaluation and eager evaluation. Strong normalization holds for MLTT (and any reasonable type theory for use in mathematics), so there is no formal difference between them. However, if the proof
f of A → B is complex and the proof
a of A is large, we find quite a distinction between the unevaluated
f a and the corresponding evaluated proof of B.
Maybe this is just a question of definition of “proof”, and both make sense. I can also imagine there being differing opinions by different philosophers, so I'm interested in any answers.