So Hilbert famously asked for a formalization of all of mathematics which was computationally decidable. Gödel is credited with shattering the idea that "all of mathematics" can be formalized. After all, one can't even formalize all of elementary arithmetic. But the decision problem (Entscheidungsproblem) was still considered open until Church/Turing.
I've read a fair number of popular accounts of this period. They always end with "finally the unsolvability of the Halting Problem completely shattered Hilbert's dream" and no further explanation. I feel like there are a few steps missing here. Why exactly does the unsolvability of the Halting Problem go against the decision problem?
Presumably the argument is: a formalization of all of mathematics has to be able to formalize Turing machines. Hence, it contains sentences of the form "Turing machine T halts". A decision procedure for such a formal system would therefore solve the Halting Problem. And that can't be done.
But Turing machines were a very new invention at the time. Why didn't people try to rescue the decision problem by saying Turing machines weren't an objective for formalization? And why does nobody seem to feel obligated to show that the decision problem can't be solved regardless?