[kriro]

Looking at the table of contents, I see no mention of Gödel/incompleteness theorems or limitations which is not a great sign. It does look well structured though but I'd probably recommend just going with "Introduction to Logic" by Tarski and "Metalogic. An introduction to the metatheory of standard first order logic." by Hunter. Those served me well and are fairly understandable for a non-mathematician (imo).

Alternatively hop straight into Prolog (Art of Prolog, Craft of Prolog).

[fmajid]

How are Gödel's incompleteness theorem relevant to the working programmer?

[xelxebar]

Programs as data.

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...

[1]:https://www.youtube.com/watch?v=dwNxVpbEVcc

[cubefox]

> I'd probably recommend just going with "Introduction to Logic" by Tarski and "Metalogic.

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.

[alfiedotwtf]

Even though I was doing Prolog (well… Mercury) every day at work, I struggled to get past the first few chapters of Art of Prolog :(

I guess I’m more mature now, so I’ll have yet another attempt… but I don’t like my chances!