Alternatively hop straight into Prolog (Art of Prolog, Craft of Prolog).
Proofs of incompleteness theorems, the halting problem, Rice's theorem etc. all share a diagonalization structure. The keyword here is Lawvere's fixed-point theorem[0], but it's a bit of abstract nonsense, so here's a good accessible video on the topic[1].
I'm not sure the incompleteness theorems themselves are immediately and directly applicable to software development, but I find that having several examples of diagonaization proofs bouncing around in my head makes the Lawvere structure apparent. Since proofs are just programs, the pattern is surprisingly pervasive. Futamura projections are one incarnation, which is essentially how many interpreters end up providing "compilation" of programs into standalone binaries.
[0]:https://en.wikipedia.org/wiki/Lawvere%27s_fixed-point_theore...
Those are not aimed at programmers, so very different and not a replacement. Just look at the free sample on the website. Besides, incompleteness theorems are probably irrelevant for programmers.
I guess I’m more mature now, so I’ll have yet another attempt… but I don’t like my chances!