Justify intuitionistic logic through the BHK interpretation could be problematic

Using the BHK interpretation to justify intuitionistic logic requires a discussion on what we mean by a "function" that transforms a construction of A to a construction of B. van Dalen and Troelstra writes (in Constructivism in Mathematics):

This exercise shows that the BHK-interpretation in itself has no "explanatory power": the possibility of recognizing a classically valid logical schema as being constructively unacceptable depends entirely on our interpretation of "construction", "function", "operation".

The OLT is justifying the ND-rules for intuitionistic logic using the BHK-construction, but a similar BHK based argument justifies the RAA rules as well (interpreting "function" as a classical set theoretic object).

I think this should be commented on in the text together with a discussion on what a constructive transformation could mean. I'm afraid I won't be able to do it good enough.

The issue does not name a file, test, or entry point. Start by locating the OLT's BHK justification and compare it with the cited discussion from van Dalen and Troelstra. Done means adding a clear, agreed-upon explanation of what constructive functions or transformations mean and why the classical reading is insufficient.