3 ms·
An Awesome Introduction to Program Verification with Coq
- mnemonicsloth 17y agoBetter title: Introduction to Program Verification with Coq See the site guidelines. http://ycombinator.com/newsguidelines.html http://ycombinator.com/newsguidelines.html
- davidkellis 17y agoMy master's thesis advisor (http://www.cs.ttu.edu/~rushton/ http://www.cs.ttu.edu/~rushton/) is interested in formal verification. This is the most practical and informative introduction to formal verification that I've seen yet. All the talks about formal verification using Mizar/PVS/ACL2/etc. that I've attended have been over my head and utterly impractical. The Coq documentation, even though at first glance is still over my head, is much more approachable than the Mizar documentation I've seen. Thanks for the link!