Your picture of mathematics is quite a bit more robust, so I won't deny that what you wrote here is more accurate than my "Gödel say it won't work, woe is our field!" brimstone version. So I'll explain my reasoning for invoking Gödel.
I mostly wanted to walk around the historical event I mentioned, the breaking of the Hilbert Program. At the time, it seemed that formal specification of math would provide a complete picture of what math was! Once the Program was finished then the job of mathematician would eke out into "computer" (of the abacus sort) or into other fields which interpreted the canon.
I'm not sure which death stroke was stronger, the incredible opaqueness and complexity of proof systems like ZFC or Gödel just saying what he was trying was outright impossible, but Hilbert's Program was killed before it even seriously took off, leaving the study of mathematics and the practical formalisms we use to study it pretty ad-hoc instead of grand and unified.
I'm unifying that with the fact that the way math seems to be practiced never comes from the formal language but instead first comes from imagining some kind of "mathematical object" and then taming its behavior with formalisms. You could consider them to be one and the same and argue that the difference is highly philosophical, and then this is where I'd invoke Gödel and inform you that there definitely exist things we could benefit from reasoning about that your formal language would fail to describe. This existence proof separates the classes of true things and provable things and makes their distinction more than philosophical.
Now, talking about what a "mathematical object" is gets you to the bleeding heart of the philosophy of science and epistemology. It's a tough question!
---
As a final note, ZFC is ZF + Axiom of Choice... which, yes, most practicing mathematicians just accept AoC so that they can integrate or whatever. The formal world without AoC is very sparse, but nobody has any sort of idea what the arbitrary decision means. I know that there has been some significant study of ZF-C, though it's been "impractical", I don't know if anyone is willing or capable of stating that ZF-C is in any way worse than ZFC. Impractical is a Mathematicians favorite adjective, so they're just two extant formal systems which disagree quite a lot on important things but we mostly pay attention to ZFC.
I mostly wanted to walk around the historical event I mentioned, the breaking of the Hilbert Program. At the time, it seemed that formal specification of math would provide a complete picture of what math was! Once the Program was finished then the job of mathematician would eke out into "computer" (of the abacus sort) or into other fields which interpreted the canon.
I'm not sure which death stroke was stronger, the incredible opaqueness and complexity of proof systems like ZFC or Gödel just saying what he was trying was outright impossible, but Hilbert's Program was killed before it even seriously took off, leaving the study of mathematics and the practical formalisms we use to study it pretty ad-hoc instead of grand and unified.
I'm unifying that with the fact that the way math seems to be practiced never comes from the formal language but instead first comes from imagining some kind of "mathematical object" and then taming its behavior with formalisms. You could consider them to be one and the same and argue that the difference is highly philosophical, and then this is where I'd invoke Gödel and inform you that there definitely exist things we could benefit from reasoning about that your formal language would fail to describe. This existence proof separates the classes of true things and provable things and makes their distinction more than philosophical.
Now, talking about what a "mathematical object" is gets you to the bleeding heart of the philosophy of science and epistemology. It's a tough question!
---
As a final note, ZFC is ZF + Axiom of Choice... which, yes, most practicing mathematicians just accept AoC so that they can integrate or whatever. The formal world without AoC is very sparse, but nobody has any sort of idea what the arbitrary decision means. I know that there has been some significant study of ZF-C, though it's been "impractical", I don't know if anyone is willing or capable of stating that ZF-C is in any way worse than ZFC. Impractical is a Mathematicians favorite adjective, so they're just two extant formal systems which disagree quite a lot on important things but we mostly pay attention to ZFC.