I would like to ask for literature recommendations on foundations of set theory focusing on the treatment of the concepts & the nature of metalanguage & metatheory, so the language&theory used to reason about the object theory. Especially, to what extent can one treat it or parts of it with formal rigor as in the case of formal language & theory? Unfortunately, most books on foundations of set theory sweep these aspects benevolently under the rug, and this raises the question at which "level of formalness" one should actually treat metalanguage & metatheory and if there are some works addressing this issue.
Motivation: In discussion here with Mikhail Katz I learned that usually metalanguage & metatheory are usually considered less formally then the object theory, which we treat in full formal rigorosity, ie we can pin down the the formal system associated with it, ie the formal language in which its sentences are phrased, we have syntax rules, deductive apparatus/rules of inference, etc which actually precisely dictate what we can do and what not as long as working with formal theory. Attempting that same approach to meta things - i.e. just to regard metatheory & metalanguage as another formal theory & language used to make statements about the object theory - seemingly is not so easy to establish.
One of the example indicating that there are seemingly fundamental differences between metatheory and object theory from level of formalness is eg the concept of "metalanguage integers". It appears as an intrinsic object of metatheory which seemingly has no analogon in object theory.
Recall, that object theory consists of formulae in certain formal language. If our formal theory describes set theory then it should have a formula "there exist a unique inductive set". Then, in every model of this theory there exist a set witnessing the truth of this formula, which we would call "internal integers". But note that these integers live in a fixed model; it doesn't make sense to say that the theory itself has integers.
In contrast in metalanguage one can talk about "metalanguage integers" indicating that metalanguage & metatheory happen to have less formal character.