Introductory books to theoretical computer science usually introduce a the Turing machine and some of its variants, as well as the Random Access machine as computational models. Sometimes more specialized or even exotic systems (such as quantum computers) can be found briefly sketched.
The equivalence of these models ( say two models A and B ) is usually proven by mimicing the mechanics of A with the "gears" of B and then providing "cheap" conversion functions which convert input of A to input B and output of B back to output A - the same is then done for A and B reversed.
Whereas proofs provide valid statements about well-defined mathematical objects, I don't think they prove what is ought to be proved, namely the equivalance of two computational models, because that question is non mathematically defined. I doubt that this can be done.
First of all, the conversion functions between the different input/output formats cannot necessarily be formalized as computations, because they act in "both worlds" (say binary strings and a cell setting in the game of life), and thus require a new computational model for themselves. Hence at least two further computational models are introduced. The triviality of the conversion functions doesn't seem be formalized. - One might argue that the conversions are the most vital part of the proof, because the "mimicry" of one model A within another model B has no mathematicly well-defined relation with the model A.
Second, I wonder whether the "class" of computational models can be formalized. I don't think it is a set, because, for example, you could build several Turing machines with 0 and 1 represented by arbitrary inequal sets. - One might define a category of computational models, with the arrows, say from object A to object B, present when A can be simulated by B. This raises the question what we would want the objects to be. I do not know.
I regard these points, (i) non having a formal definition for the conversion functions to be trivial, (ii) having no definition of a (Turing-equivalent) model of computation as unsatisfying.
Does anybody know whether and how this has been treated in literature so far? I am aware this touches what to understand the question of what to call "computation", but so do the usual practices in computer science anyway, in my opinion.