3 ms·
Raymond Smullyan's books can teach a fair bit about logic, up to about Godel's theorems and the halting problem (I remember To Mock a Mockingbird fondly), throu
by conistonwater 8y ago
Raymond Smullyan's books can teach a fair bit about logic, up to about Godel's theorems and the halting problem (I remember To Mock a Mockingbird fondly), through carefully written sequences of puzzles that lead up to proofs of them.
If you try to go through his books encoding the puzzles and their solutions in Coq, then you'll learn quite a lot about Coq and constructive mathematics also.
- edanm 8y agoAn interesting idea! I've long wanted to go through more of his books, and I've also long wanted to learn Coq, so that sounds like an interesting combination. Have you found it worthwhile to learn Coq?
- conistonwater 8y agoI learnt it mostly for the sake of learning something new, I didn't really think at the time whether it would be worthwhile. It's a very specific tool developed by people in very specific fields of CS (type theory, compiler verification, but I could be wrong about this), so I just never felt bad about not having a use for it myself. Encoding (a subset of) the puzzles as SAT problems for something like z3 would be an alternative to Coq.