A word of caution: This textbook can get pretty bogged down sometimes because it serves double-duty as a Coq tutorial. (It has to, because the book is literally

A word of caution: This textbook can get pretty bogged down sometimes because it serves double-duty as a Coq tutorial. (It has to, because the book is literally a Coq script, using formal theorems w/ proofs as examples and formal theorems w/o proofs as exercises.) In my opinion, the material doesn't really take off until vol 2. However, I don't want to disparage the tutorial nature too much, because learning to "think in Coq" has dramatically changed the way I reason about even traditional pencil and paper proofs, for the better.