If you want to get started with Coq there are two good resources. One is Software Foundations[sf] by Benjamin Pierce. There's also Certified Programming with De

If you want to get started with Coq there are two good resources. One is Software Foundations[sf] by Benjamin Pierce. There's also Certified Programming with Dependent Types[cpdt] by Adam Chlipala. I would say [cpdt] is more advanced than [sf], so I think it's best to start with [sf] and then start on [cpdt] if you feel up for the challenge. I have mixed feelings about Coq as a tool for software design. On the one hand I think it's feasible to use Coq to prove correctness properties of your programs. On the other hand I feel it can sometimes be extremely tedious and / or difficult to show some properties. I do believe it is the future to prove properties about parts of your program, though. Lately I have been working on brainfuck in Coq[bf] in my spare time. I have spent almost two weeks on the project now and I have been able to show that 1) the "Hello World!" program on brainfuck's wikipedia page does indeed output "Hello World!"[hello], and 2) the correctness of a simple compiler from arithmetic expressions (with +, -, and *) to brainfuck[compiler]. The project is more than 1000 lines of code. I must admit some of the code / proofs are messy and could probably be shorter, but I think it does indicate how much work it requires (and how messy brainfuck is!) [sf]: http://www.cis.upenn.edu/~bcpierce/sf/ http://www.cis.upenn.edu/~bcpierce/sf/ [cpdt]: http://adam.chlipala.net/cpdt/ http://adam.chlipala.net/cpdt/ [bf]: https://github.com/reynir/Brainfuck https://github.com/reynir/Brainfuck [hello]: https://github.com/reynir/Brainfuck/blob/master/bf_theorems.v#L113 https://github.com/reynir/Brainfuck/blob/master/bf_theorems.... [compiler]: https://github.com/reynir/Brainfuck/blob/master/ae_compiler.v https://github.com/reynir/Brainfuck/blob/master/ae_compiler.... Edit: I just remembered this talk by Wouter Swierstra where he proves some correctness properties for the core of xmonad: http://www.youtube.com/watch?v=jqaOU8kqykg http://www.youtube.com/watch?v=jqaOU8kqykg (unfortunately I can't find the slides at the moment).