The use of coding in RM is well-known. I have gathered some example theorems for which the logical strength changes considerably if we change “second-order code for continuous function” to “third-order function that is also continuous”. I am thinking of e.g. the Heine, Weierstrass, and Tietze theorems on separably closed sets, but also more recent results on the Ekeland variational principle. The problem seems to be that certain second-order codes do not give rise to third-order functions in e.g. Kohlenbach’s base theory, i.e. there are “too many” codes.
The associated paper is here:
Can anyone think of more theorems of this kind?