One of the reasons for the existence of formal logic systems is to establish the foundations of mathematics. To have all theories constructed and proven using particular syntactic rules based on a proof theory.
If so, how do we prove that a formal logic system satisfies a certain property, Soundness for example? We can't use the rules of deduction defined in our formal logic system on itself (we haven't established its validity yet), so we have to write a proof in "human" language before we can use the system.
How can this make sense? Foundations of mathematics now rely on "human" informal language proofs at its base.