Any modern course on formal methods in software design should at least mention modern tools like coq, however, in this course there're no mention of them.
Coq is an excellent tool for software-assisted theorem proving, but it can also be good to know how to do certain things without the help of a computer. This course is about a theory of programming that's practical and simple enough to use on its own, without support from a tool like Coq, just like one might calculate the answer to a multiplication problem on pencil & paper, without using a calculator.
For all its simplicity, the theory is still general: it deals with parallel, sequential, probabilistic, deterministic, standalone, and interactive programs, as well as time (incl. real-time) and space bounds. It can even be used as a rigorous way to solve probability problems by hand, by writing a program to simulate the scenario and proving what its result is. (http://www.cs.toronto.edu/~hehner/ProPer.pdf)
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?
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!)
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 (unfortunately I can't find the slides at the moment).
have you any experience with alloy? http://alloy.mit.edu/alloy/ - that seems like it's aiming for a middle-ground somewhere between coq and crossing your fingers.
