I know that the set of provable propositions in a sufficiently complex formal system is recursively enumerable but non-recursive, and so no Turing Machine could decide all the propositions that could be decided from the axioms and rules of procedures of the system.
But in his book "Shadows of the Mind", Roger Penrose uses a version of Gödel's theorem based on Turing Machines (or computations generally). He says that for a given Turing Machine H which is supposed to take as input another Turing Machine M acting on n, H sometimes determines whether M halts or not. From then, he shows that there always is a certain computation k (acting on input k by diagonal slash) which H cannot handle: H can't determine whether the computation k halts or not, when in fact it does not halt.
Is this proof different than the standard Gödel theorem? Does this show a kind of equivalence between algorithms and formal systems?