I'm currently in Prof. Pierce's class at UPenn! Can confirm this is a great book, and we literally work through the exercises. Taking this class AFTER using Scala in industry has really put a lot into context. It's so easy to start too - download CoqIDE or ProofGeneral and get to it!