Well, I was inspired by the top comment which said "doing logic surely feels like programming". Not a coincidence, they are a very same thing - CHI. Book on logic shouldn't beat around that bush (because frankly, mathematicians know better than programmers); it should address it head on, that using classical logic as a metalanguage in programming is more of a historical accident, and we could use pretty much any programming language as well. Which means at least some metalogical reasoning could be and should be automated, an interesting fact for any working programmer.