What's the problem in logic in defining satisfaction in terms of a formal translation (and thus obtain the rules as theorems)?

The formal definition of "$\models_{\mathcal{A}} \varphi[s]$" based on satisfaction rules is the definition of the "translation of $\phi$ determined by $\mathcal{A}$ and $s$".

If you're not convinced, I suggest you write out in detail the recursive definition of "translation" that you have in mind. You'll find it's exactly the same as the recursive definition of $\models$, just using different notation.

Let me try to clarify my answer in response to the comments below. I'm making two claims here:

(1) When Enderton writes informally about a "translation", he's referring to the definition of satisfaction (which "translates" each logical connective to its meta-language counterpart) and nothing more.

(2) If you carefully write out the formalization of "translation" you have in mind, you'll find that it differs from the definition of satisfaction only in notational choices.

Now in the comments, you wrote that what I said is false because "it forgets that the right hand side can be seen as the construction of an expression". Here I'll reiterate Karl's point from the comments. If this "expression" is a formula in the meta-language, then it is not itself a mathematical object, so theres no way formalize the idea of "constructing" it. All we can do is give a meta-language definition like the recursive definition of satisfaction. On the other hand, if your "expression" is not a formula in the meta-language, then it is a formula of some object language, and you've just pushed off the problem to defining satisfaction for that language.