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 co

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 http://www.cs.toronto.edu/~hehner/ProPer.pdf)