Video tutorials for the Coq proof assistant
- 22 February 2011
- General
Next week I am going to a meeting where I am supposed to give a tutorial on the Coq proof assistant. Inspired by the Catsters, I decided to prepare the material in the form of screencasts. You can find the first few tutorials on Youtube in my “Coq tutorials” playlist. So far I have:
- Obtaining and installing the Coq proof assistant
- How to use CoqIDE
- How to use Coq with Proof General
- A first proof with Coq (Frobenius rule)
- The dual Frobenius rule, part 1
- The dual Frobenius rule, part 2
- Currying and uncurrying, part 1
- Currying and uncurrying, part 2
You should turn on the high quality HD stream when you watch these. Feedback is welcome (and easy to provide on Youtube). I find it very, very difficult to listen to my own voice. I hope to have many more lectures soon, but I am starting to feel out of my depth, so if anyone wants to help they are welcome!
I am making screencasts with
Screenium on my Mac, which is just one of many available options. Preparation of a screencast takes less time than preparation of equivalent written notes or slides, as long as one is not obsessed with making everything perfect. In fact, I think it is important not to make tutorials perfect. In a screencast the viewer can see how I make mistakes and, more importantly, how I discover and fix them. It still takes me two or three takes before I am happy with a screencast, but all in all the process is becoming more streamlined with each next tutorial.
I have learnt a couple of tricks. The “pause” button is my friend when the phone rings or I need to think for a moment what to say next. It takes less time to start over than to try to edit out mistakes afterwards. A screen cast must be short. There must be a central message, but often I find it convenient to explain “on the side” various details which do not easily fit anywhere.
Somehow the whole process feels organic. There is less global planning than in teaching a course, but some planning is still needed. There are non-traditional ways of organizing tutorials into playlists. For example, other people can combine screencasts from various sources and create their own tracks. I think there is a lot of potential.
Screencasts are ok for computer-sciency themes, such as Coq and programming, but for real math, I will have to make videos of handwriting. The Catsters stand in front of a blackboard in their videos, but I would like to try pencil and paper with our departmental document camera. We will see how that goes.