4 ms·
Chlipala's book is a decent one, but it's oriented towards software verification, coq, and the use of tactics (which I would consider anti-pattern). Software F
by solomatov 9y ago
Chlipala's book is a decent one, but it's oriented towards software verification, coq, and the use of tactics (which I would consider anti-pattern).
Software Foundations is a good introduction to Coq and proofs, but overall is quite basic, and it also hides many details of how type theory works, so it's more of a hands on tutorial.
TLA+ is just a tool which basically does its job by exhaustively searching a space of possible solutions trying to find counterexamples. It works in some limited cases but doesn't work generally for any mathematical theorem.
- nickpsecurity 9y agoI bring up TLA+ because many people have quit trying to learn Coq because it was so hard with little perceived benefit. TLA+ has a high ratio of benefit for work put in. It also shows that abstract modeling can knock out deeper errors than regular tests or sometimes review. That makes it a nice, intermediate step toward stuff like Coq. Just a hunch a few of us have. :)
- pron 9y ago> TLA+ is just a tool which basically does its job by exhaustively searching a space of possible solutions trying to find counterexamples. It works in some limited cases but doesn't work generally for any mathematical theorem. Nope. TLA+ is a rich mathematical formalism, that includes a full-fledged proof assistant. It is, however, focused on verifying software rather than arbitrary mathematical theorems. There is also a model checker for TLA+ that can check your theorems (about finite cases of programs) at the push of a button. In practice, model checkers works in more cases than manual proofs, as manual proofs "fail" much more often, simply by being far too laborious; a model checker would verify in days what may take you months or more to manually prove.