Metalanguage & Metatheory in FoST

Question

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.

Answer 1

There is an article by Nelson that makes some related comments in the context of the distinction between potential and completed infinity:

Nelson, Edward. Hilbert's mistake. 2007

Here Nelson writes:

Let us distinguish between the genetic, in the dictionary sense of pertaining to origins, and the formal. Numerals (terms containing only the unary function symbol S and the constant 0) are genetic; they are formed by human activity. All of mathematical activity is genetic, though the subject matter is formal.

Numerals constitute a potential infinity. Given any numeral, we can construct a new numeral by prefixing it with S.

Now imagine this potential infinity to be completed. Imagine the inexhaustible process of constructing numerals somehow to have been finished, and call the result the set of all numbers, denoted by N.

Thus N is thought to be an actual infinity or a completed infinity. This is curious terminology, since the etymology of “infinite” is “not finished”.

Notice Nelson's reference to "human activity" in describing numerals (which seem to be metalanguage integers).