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?
You need to be a little careful here: some formal systems are weak enough that we can easily decide the truth of any proposition. For instance, a formal system describing some particular finite structure.
If a Turing machine halts, there's a proof that it halts which is just the sequence of steps that it took.
On the other hand, you can build a Turing machine that hunts for a proof of any proposition (by searching all strings in an infinite loop to check if they're valid proofs, and also proofs of that particular proposition) and halts if it finds it.