I agree that Turing Machines feel more natural to programmers than first-order logic (although "natural" doesn't necessarily mean "rigorously proven"), but the

I agree that Turing Machines feel more natural to programmers than first-order logic (although "natural" doesn't necessarily mean "rigorously proven"), but there are no leaps of faith involved in Gödel's construction. You can write down "P is provable" as a first-order sentence of arithmetic (which involves some number theoretic tricks), and you can also do the diagonalisation trick that gives you self-referentiality. That's really all you need.