I'm looking for an introductory book on mathematical logic that also discusses an implementation of its logic in a proof assistant. It seems to me this would be a great way to learn mathematical logic, since many concepts would become very clear and concrete when implemented in a computer program. But I have never seen such a book.
Preferably, the book would introduce the language of the proof assistant assuming no prior knowledge, and encourage the reader to use it at various points.
I like the answers posted so far, and want to keep this open for a while to collect other recommendations in one place. However, after opening it, I also found the following excellent resources linked in this question, namely this list of resources and this book/compilation of notes by Jeremy Avigad. These resources seem like the type of thing I was looking for, and might be helpful to others who stumble on this post.
One feature I would really like to see, which I haven't seen in the suggestions so far, is a book that also formalizes its meta-logic within a proof assistant. For example, I would love a book that proves (for example) a soundness theorem, and shows how such a proof could be implemented with a proof assistant.
Then again, I'd be surprised if such a resource exists, since no mathematical logic books (that I've seen) even mention the idea of formalizing meta-logic.