I'm reading up on Gödels constructible universe L in the book "Constructibility" by Devlin, and by comparing his text with texts like Kunen and Jech, there is one thing in particular that he's doing differently: internalizing LST (that is, the language $\{\in\}$) inside set theory itself.
To give you a brief picture of what he does, his construction is roughly to interpret every logical symbol (connectives, variables, parentheses) as natural numbers inside set theory itself, and formulas as sequences of natural numbers, again inside set theory. He proceeds to prove that on transitive sets, this interpretation coincides with the meta-mathematical one via LST (for $\Delta_0$ formulas; that is, formulas where every quantifier is bounded). He spends an awful lot of time on this, and I cannot seem to see what he gains from such a construction.
My question is then what such an internalized construction achieves? Is it so that theorems about formulas of ZFC can "make more sense" - that no need of meta-mathematical theorems is needed? Mere convenience? Philosophical issues? It doesn't need to specifically be about Devlin's construction, but more about an arbitrary internalization of set theory.
I apologize in advance if this question is too vague, but I tried to make it as specific as possible.
There are several reasons why we want to code LST (or languages in general) within set theory (or whatever strong formal theory we are working with).
You need to do this to prove the incompleteness theorems, and any relative consistency result; in fact, you need it to even formulate these results. After all, to express $\mathrm{Con}(T)$ we need a formal counterpart for $T$, and an internal formalization of first order provability.
It is also less awkward to describe the constructible hierarchy if we can talk directly about formulas and satisfaction rather than Gödel operations.
Actually, the ability to discuss satisfiability becomes more crucial as we delve into more technical arguments. A common combinatorial technique in set theory consists of starting with an initial segment of the universe that satisfies a large fragment of set theory, and then consider a countable elementary substructure. The fact that the structure is countable and elementary is used explicitly to derive combinatorial information about the statement at hand, and then transfer this information back to the universe itself. Naturally, in specific instances, we do not need satisfiability in general, and can instead argue explicitly in terms of whatever functions we need our structures to be closed under. But this is cumbersome in many cases, and distracts from the combinatorial core we are really after.
As for the constructible hierarchy, it is not just $L$, but many other structures that are defined explicitly in terms of definability and information about Skolem hulls. Besides, the explicit formalization of the satisfiability relation may shed some light on the technical difficulties that prevent us from carrying out Lowenheim-Skolem arguments with proper classes in general (something that can then be formalized via Tarksi's theorem of undefinability of truth, for example).