It depends on what level one is working. Suppose that I prove
mathematically that there is a proof of theorem X, even prove it
constructively. The computer code generated by following the procedure
outlined in my proof may be so large as not to be implementable.
I'm doing metamathematics, but it is not implementable directly.
Of course, this can be avoided by making the theory in which
metamathematical reasoning is to be carried out sufficiently weak;
but I don't think that PRA is weak enough to forbid metamathematical
results of this kind (comments on this question are invited?) One's
metamathematics needs to be not only constructive but "feasible" in
some sense to make the situation I describe above impossible.
Does this clarify my point?
--Randall