3 ms·
I took a university class on said book last year, held by one of the authors Prof. Tobias Nipkow. Its a fascinating introduction into general program semantic
by itsphilos 6y ago
I took a university class on said book last year, held by one of the authors Prof. Tobias Nipkow.
Its a fascinating introduction into general program semantics, formal analyses and proofs for program properties.
During the lecture I struggled somewhat as I didn‘t really have sufficient background knowledge for it to run smoothly.
But all the concepts are supported by, well, concrete examples which you can immediately try to solve in Isabelle. So I definitely recommend giving it a go!
It was an eye-opening experience for me, especially since I never really looked into formal program analysis.
- max_ 6y agoI would like to get into formal methods but I am kind of confused. What's the difference between TLA+, Coq & Isabelle? Is there one should I prefer over the other? Or do they individualy satisfy distinctive purposes?
- zaik 6y agoI am no expert, but Coq and Isabe le "feel" very similar at first, but Isabelle seems to provide much more powerful tools for proof automation than Coq. Isar, Isabelle's proof language, tries to be close to natural language proofs which makes it more intuitive. I really wish Coq had equally powerful automation tools and a more intuitive proof language, because it feels much more of a solid language and I really liked that the clear relation of types <-> statements, terms <-> proofs, type checking <-> proof verification; including the ability to print the raw proof terms of theorems.