I've done so far a few courses in logic and formal verification, and I've always wondered: mathematical logic, at least as Hilbert envisioned, tries to model mathematics. Formally define what a "true" statement is, or why proving something (at least in a sound system) makes it true.
But, every logic course uses mathematics in its essence. The use of sets, functions and series' (as with inductive groups, for example) - is already mathematics, in a field that tries to model exactly that.
Isn't that circular logic?
It is a common misconception many logic students pass by.
Let us start with an example: Every microprocessor we use has its own design, and we can implement it in different ways: Either physically with silicon wafers, virtually with emulators, or even over Minecraft. Nobody says the design of a microprocessor is circular or contradictory. However, people become confused if a "microprocessor" becomes a "formal theory."
Formal theories, like first-order logic, set theories, or type theories can be viewed as sets of axioms and formal rules. We can implement them as computer programs (like Coq or Lean, which implement a type theory) or over another theory (as a formal theory, an interpretation, or a model.) Mathematical logic handles formal theories as objects implemented over a metatheory, and we can ask what can hold for 'implemented' formal theories.
This line of understanding collides with a common belief that mathematical logic is a field trying to build up mathematics from the ground. It was true that mathematical logic in the early 20th century focused on building a theory ensuring the consistency of mathematics. However, it changed around the advent of Hilbert's program and the incompleteness theorem.
Hilbert formulated a program for defining a complete foundation for mathematics, and he assumed that the 'perfect' foundation should satisfy some desirable properties (like soundness and completeness.) It might be disputable that "we proved a completeness of $T$ from a metatheory" ensures "$T$ is complete indeed in the reality" (The word "reality" is also quite ambiguous, although it should be clear in the Platonist view.) However, establishing the completeness of $T$ over some metatheory is good evidence of the preference of $T$ over other theories without any justification.
However, Gödel proved that we cannot formulate a complete theory (more precisely, sound, complete, and recursively axiomatizable extension of $\mathsf{PA}$.) Hilbert's program turned out not to work, but Hilbert's view on analyzing a formal theory over mathematics turned out to be useful.
By that tendency, modern logic textbooks teach students about the properties of formal theories over a metatheory, and they do not try to build a formal theory encompassing the entire mathematics.