[randomswede]

If your question is "does Gödel Incompleteness have practical applications", my answer is "probably". Not necessarily directly, but indirectly it has inspired much other work.

One of the things it inspired was Turing's work on uncomputable numbers. It turns out that computability and incompleteness are intertwined, which at least I find interesting. And without the "uncomputable numbers" malarkey, I wonder if the Turing Machine formalism would exist (answer, "probably, but maybe looking different and with another name"). And, well, the Halting Problem is essentially Gödel Incompleteness (imagine handwaving here).

As for proof systems, again, the answer is "probably". Knowing that there are true, unprovable, statements in a formalism is something that informs how you approach it, you need to put a limit on how far to go before you say "I don't know" and taht is in and of itself important.