2 ms·

Hmm, that is unfortunate. However, since my university recently canceled its only class that covered formal methods in any depth, I haven't been able to find an

Hmm, that is unfortunate. However, since my university recently canceled its only class that covered formal methods in any depth, I haven't been able to find any great options for learning about this area in a structured way. Perhaps you could provide an alternate, superior option?

reycharles 13y ago
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).
- andrewcooke 13y ago
  have you any experience with alloy? http://alloy.mit.edu/alloy/ http://alloy.mit.edu/alloy/ - that seems like it's aiming for a middle-ground somewhere between coq and crossing your fingers.

reycharles 13y ago

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).

andrewcooke 13y ago
have you any experience with alloy? http://alloy.mit.edu/alloy/ http://alloy.mit.edu/alloy/ - that seems like it's aiming for a middle-ground somewhere between coq and crossing your fingers.