This proof using Turing machines is indeed very slick! Its elegance is balanced by its nonconstructiveness: Gödel's proof yields an explicit example for an unprovable statement (namely a formal rendering of "this statement is not provable"), while the Turing machine proof doesn't.

Also let me add a remark on a certain subtlety: Step 3 only works if we assume that, if a claim about the halting behaviour of Turing machines has a proof in the studied formal system, then it's actually true.

This assumption is believed to be warranted for the standard formal systems of mathematics such as Peano Arithmetic (PA) or Zermelo–Fraenkel set theory (ZF), but Gödel's proof also applies to formal systems for which this assumption doesn't hold, or for which the assumption does hold but cannot be proven in a weak metatheory.

These systems are typically not very useful as vehicles to carry out formalized mathematics, but they are nevertheless very interesting and fundamental to the study of logic. An example for such an anti-real formal system is PA adjoined by an axiom expressing that PA is inconsistent.