3 ms·
Off topic, but I'm an engineer whose math extends (shakily) into basic proofs (though I'm rusty). I tinkered quite a bit with Lean a couple of years ago and fel
by joshmarlow 4y ago
Off topic, but I'm an engineer whose math extends (shakily) into basic proofs (though I'm rusty). I tinkered quite a bit with Lean a couple of years ago and felt comfortable with it as a language, but I don't actually grok how to use it effectively for proving theorems (I'd love to get into formal verification).
Do you have any recommendations for getting started? Something like a "Proofs for Hackers"?
- opnitro 4y agoSoftware Foundations is always a great place to start! (https://softwarefoundations.cis.upenn.edu/ https://softwarefoundations.cis.upenn.edu/) It uses Coq not Isabelle, but it's a great starting point and contains a ton of useful information. The book is one large literate program, so it's easy to follow along and do the exercises.
- tombert 4y agoSoftware Foundations (mentioned in a sister comment) is great, and highly recommended. If you want something more Isabelle-focused, the Concrete Semantics book is pretty good [1]. 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/ http://concrete-semantics.org/ [2] https://lamport.azurewebsites.net/video/videos.html https://lamport.azurewebsites.net/video/videos.html