The long term goal is to be able to use Coq or Isabelle to prove some small piece of software.
Link:
https://books.google.com/books/about/Fundamental_Proof_Metho...
Link:
https://books.google.com/books/about/Fundamental_Proof_Metho...