18 ms·
This looks really cool! I've never worked with Coq myself, and really, the process described here still looks much too convoluted for practically proving nont
by tomsmeding 9y ago
This looks really cool!
I've never worked with Coq myself, and really, the process described here still looks much too convoluted for practically proving nontrivial amounts of code correct. But it looks like lots of fun too! And it is sort-of the holy grail of computer science, writing code and being able to prove it correct instead of just testing it with maybe-or-maybe-not enough test cases.
In practice I find that Haskell itself already prevents a lot of bugs, but of course in functions like the one dissected here, logical errors are still easily made.
I'll definitely look into Coq one of these weeks.
- lcdoutlet 9y agohttp://www.cl.cam.ac.uk/~jrh13/hol-light/ http://www.cl.cam.ac.uk/~jrh13/hol-light/ The author John Harrison who works at Intel has used his theorem proving application hol-light in doing verification on large code bases.
- neilparikh 9y agoYou might already know about this, but if you're looking to learn Coq, I would recommend the Software Foundations series (https://softwarefoundations.cis.upenn.edu/ https://softwarefoundations.cis.upenn.edu/).
- harveywi 9y agoI started with Certified Programming with Dependent Types (http://adam.chlipala.net/cpdt/ http://adam.chlipala.net/cpdt/). If you are more interested in programming, consider trying Idris (http://idris-lang.org/ http://idris-lang.org/). Edwin Brady, the language designer, wrote a great book that I would recommend called Type-Driven Development with Idris (https://www.manning.com/books/type-driven-development-with-idris https://www.manning.com/books/type-driven-development-with-i...).
- nickpsecurity 9y agoI have a stock recommendation for this if you want to learn formal methods to hopefully prove some useful programs. It might also apply if you want to do it for fun but don't want to get weighed down too much. https://news.ycombinator.com/item?id=15781508 https://news.ycombinator.com/item?id=15781508
- tomsmeding 9y agoThanks for mentioning, will look at that as well. But I think I'd like to try Coq anyway :)
- agentultra 9y agoIf you're considering Coq but haven't started I'd also consider Lean[0]. The documentation isn't as great but the main tutorial is decent. It also doubles as a practical programming language. And the community is active and helpful. I've always found Coq to be a little impenetrable. I don't know what makes Lean more accessible to me but I've found it much easier to get into. [0] https://leanprover.github.io/ https://leanprover.github.io/