[Turing 1936] pointed out that the theorem of computational undecidability of the halting problem is rather different than
Gödel's theorem of the inferential undecidability of I'mUnprovable. In strongly-typed theories, computational undecidability of the halting problem can be used to prove inferential undecidability but not vice versa because the proposition I'mUnprovable does not exist.
