Nevertheless, PRA or something alike is accepted by many people to be able to express correctly the basic properties of finite objects like formulas or proofs. Therefore it can serve as a tool to express things like "P is a proof of sentence A from theory T in logic L" (NOT: "A is a logical consequence of T").
I doubt, whether such a translation to PRA is necessary for the acceptance of QED. One might be able to encode proofs from other systems in PRA in linear time and the authors of the proofs may feel better if the encoding went through without errors. But who would by the product - i.e. the encoded proof? (Contrary to David I believe that a translation back from PRA into other calculi will take at least exponential time [I know that this happens even for translations between fairly similar calculi like Modified Problem Reduction, Simplified Problem Reduction and Model Elimination]. The reason is that the structure of a proof contains implicitely information that has been useful in the specific calculus to build that proof. This information is lacking in a proof produced with another calculus).
HOWEVER I have no doubt, that the development of a central bookkeeping system is very useful for the development of QED because it encourages cooperation and exchange.
Ingo Dahn