This may be a naive question, but here goes. (Edit -- it is not getting upvotes, but nobody has offered a response either; perhaps the question is more difficult, obscure, or unclear than I thought?)
Gödel's First Incompleteness Theorem can be proven as a corollary of the undecidability of the halting problem (e.g. Sipser Ch. 6; blog post by Scott Aaronson).
From what I understand (confirmed by the comments), this proof does not depend on the Church-Turing thesis. We derive a contradiction by showing that, in a complete and consistent formal system, a Turing Machine could solve the halting problem. (If on the other hand we had just shown that some effective procedure could decide the halting problem, we would need to also assume the Church-Turing thesis to get a contradiction.)
So, we might say that this result provides a bit of intuitive support for the Church-Turing thesis, because it shows that a limitation of Turing Machines implies a universal limitation. (Aaronson's blog post certainly supports this view.)
My question is whether we can gain something more concrete by going in reverse: What formal implications do Gödel's theorems have for the Church-Turing thesis? For instance, it seems intuitively possible that the First Incompleteness theorem implies that no effective procedure can determine if an arbitrary Turing Machine halts; the reasoning might go that the existence of such a procedure implies ability to construct a complete $\omega$-consistent theory. Is this correct? Are there any results along these lines?
(I'm asking out of curiosity -- I don't study logic myself -- so I apologize if this is well-known or not research-level. In that case, consider this a reference request! Thanks for any comments or responses!)
Question that sounds related, but isn't: Church's Theorem and Gödel's Incompleteness Theorems
EDIT: I'll try to make the question more clear! First -- my naive intuition is that Gödel's Incompleteness should imply at least some limitations on what is or is not computable. These limitations would be unconditional, i.e., they should apply to all models of computation rather than just Turing Machines.
So I am wondering if this is the case (there must be some implication, right?). Assuming it is, I'm most curious about how it impacts the Church-Turing Thesis -- the notion that anything effectively calculable can be computed by a Turing Machine. For example, it seems possible that the existence of an effective procedure for deciding whether a Turing Machine halts would contradict the First Incompleteness Theorem. This result would demonstrate that no possible method of computation can be "much" more powerful than Turing Machines; but is this result true? I have a couple similar questions in the comments. I would be very interested to hear an answer to one of these questions, a pointer to an answer in the literature, an explanation of why my entire reasoning is off-base, or any other comments!