3 ms·
I liked the little summary at the end: > So in all it took 1.5 years to learn Coq well enough and to find the right abstraction, and 2 weeks to do the actual w
by tikhonj 11y ago
I liked the little summary at the end:
> So in all it took 1.5 years to learn Coq well enough and to find the right abstraction, and 2 weeks to do the actual work.
That matches what other people have told me about Coq: the learning curve can be brutal, but you can be surprisingly productive once you get over it. (To be fair, this sort of problem also feels like a really good fit for Coq—proving theorems in more developed sub-field of mathematics is much harder.)
A pretty cool project all around!
- rtpg 11y agoI've had only a little exposure to Coq, but for the life of me I could not understand how to use it. I mean on the practical level, not the conceptual level. I know people talk about it as a theorem-prover, but how do I actually _use_ that? This might be due to my general lack of exposure to theorem provers in general, but I can't wrap my head around how I can use this to make my programs better in a practical environment (despite my total buy-in to the concept)
- nmrm2 11y agoCheck out http://adam.chlipala.net/cpdt/ http://adam.chlipala.net/cpdt/
- thinkpad20 11y agoAlso (and IMO this one is a little more well-structured) the Software Foundations course[0]. Especially when supplemented by Pierce's excellent lectures, available on youtube. [0]: http://www.cis.upenn.edu/~bcpierce/sf/current/index.html http://www.cis.upenn.edu/~bcpierce/sf/current/index.html