Coding is obviously a fundamental tool in reverse mathematics, and practitioners take care to both demonstrate the correctness of their coding mechanisms and point out their limitations. Harvey Friedman posted on the FOM mailing list in 2004 (see [1] and [2]), prefacing the mathematical part of his first posting with the following.

For a wide variety of mathematical statements, the "correctness" or "appropriateness" of the coding used is completely unpoblematic, and goes virtually unnoticed. Part of the reason why it goes virtually unnoticed is that such coding mechanisms - in such unproblematic cases - are essentially the same as those that occur in virtually all aspects of recursion theory, in proof theory, and at least the finite part of set theory.

For other mathematical statements, the "correctness" or "appropriateness" of certain coding mechanisms is, in varying degrees, controversial. The main reason for this controversy is the presence of alternatives that seem equally reasonable, but are "substantially different".

The judging of the "correctness" or "appropriateness" of coding mechanisms has largely been of an informal, even sometimes polemical, nature. Here we wish to present some formal criteria that should go far in clarifying the issues, and open up new research programs.

I'm curious to know whether such new research programmes have indeed opened up, or whether there has been any further work in this area at all. I couldn't find anything by Googling "Coding in Reverse Mathematics" except an abstract for a talk by Friedman in October 2004.

[1] Friedman, H. Coding in Reverse Mathematics 1. FOM mailing list, 2004.

[2] Friedman, H. Coding in Reverse Mathematics 2. FOM mailing list, 2004.