Response to 2013/14 survey feedback.
The course ran in 2013/14 and is running in 2015/16. (It did not run in 2014/15 due to illness.)
Experience with the course in 2013/14 showed that students found using the Coq proof assistant challenging but rewarding. The final exam was given online with Coq. Of the nine students enrolled in the course, eight received perfect marks. (The ninth student had not done all of the biweekly assignments.) This is what one should expect, since the computer checks that each proof is valid, and hence contains no errors.
I thought the 2013/14 course went well, and expect 2015/16 to be even better. The theory we will learn is directly relevant to programming language ideas seeing wider use in industry, including functional, concurrent, and distributed programming. We will learn exciting ideas, work hard, and have a lot of fun. See you there!
Philip Wadler, September 2015.