I 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

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