If you are already familiar with Coq or even Ocaml/Haskell style programming. I really believe, the volume 3 of SF series is a more polished and more approacha

If you are already familiar with Coq or even Ocaml/Haskell style programming. I really believe, the volume 3 of SF series is a more polished and more approachable book. https://softwarefoundations.cis.upenn.edu/vfa-current/index.html https://softwarefoundations.cis.upenn.edu/vfa-current/index.... I am halfway through the first book (doing ALL exercises), I hope by next year end I would really like to finish vol 3. This Isabelle books seems to cover more ground though.