Do you have any recommendations for getting started? Something like a "Proofs for Hackers"?
Do you have any recommendations for getting started? Something like a "Proofs for Hackers"?
Not exactly the same, but if you want something a bit more approachable than Isabelle or Coq or Agda, it might be worth looking into TLA+. That can introduce you to predicate logic and state machines and set theory if you're not already familiar with them, and TLA+ is a lot more programmer-centric and less pure-mathey than Isabelle. TLA+ offers model checking for "brute force" verification, and also offers a formal proof system called TLAPS. Lamport's talks on TLA+ are quite good [2], and I found that learning Isabelle was a lot easier once I had a lot of practice with TLA+.
[1] http://concrete-semantics.org/ [2] https://lamport.azurewebsites.net/video/videos.html