Logic in CS: Descriptive Complexity and Curry-Howard

If you're a CS person and you've ever wondered why formal logic matters to you, here are two answers that I've found so far.

First, logic is useful in type theory, via the Curry-Howard isomorphism. Unfortunately, the meaning of "useful" here is pretty weak, since most type systems, even the advanced ones, aren't really capable of saying anything that's very interesting from a logic point of view. But we'll get there. In the meantime, look at proof assistants like Coq and languages with dependent types like Epigram.

Second, logic is useful in complexity theory, via descriptive complexity. If you ever find yourself thinking about things like non-finite-state model checking, or knowledge representation, or various other AI-ish topics, then descriptive complexity can serve as a quick cheat sheet for thinking about what the consequences would be if you added a new level of expressiveness or power to your system.

If you know of other applications for logic in CS, please share by adding a comment.