What's the problem in logic in defining satisfaction in terms of a formal translation (and thus obtain the rules as theorems)? Enderton's  A Mathematical Introduction to Logic,  p. 83, gives an informal definition of satisfaction (I paraphrase):

$\vDash_{\cal A} \phi[s]$ iff the translation of $\phi$ determined by the structure ${\cal A}$ and the assignment $s$ is true.

Next, Enderton gives the formal definition based on satisfaction rules. Am I correct to say that these satisfaction rules can be obtained as theorems from the informal definition, after the translation of a formula is defined?  The idea for the definition of the translation is simply to recursively translate the sub-expressions and recombine them as in the overall expression.
Let $\phi^{{\cal A},s}$ denote the translation of $\phi$ given ${\cal A}$ and $s$. It seems that the satisfaction rules are theorems of the informal definition of satisfaction assuming the above recursive definition of $\phi^{{\cal A},s}$. For example, consider the rule  $\vDash_{\cal A} \neg \phi[s]$ iff $\neg (\vDash_{\cal A} \phi[s])$.  If we apply the informal definition, this becomes $(\neg \phi)^{{\cal A},s}$ iff $\neg (\phi^{{\cal A},s})$, which can clearly be proven given the definition of translation.
Note added: An answer below says that a motivation to avoid a translation function is when we need to make a link with a language that is informal and thus could not be the target of the translation. This raises the question at another level.  In which way less formalization of the semantic can help make the link with an informal language? To put it in another way, how would we know that the semantic matches with this informal natural language? One could argue that, on the contrary, more formalization, thus a formalization of the semantic, could only help to explain a connection. Though, of course, given that the natural language is informal, we will never have a rigorous description of the connection.
 A: 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.
