Mathematics and Computation

A blog about mathematics for computers

Video tutorials for the Coq proof assistant

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:

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.

Comments

Filip Nikšic

That's one great tutorial. Thank you!

Thanks for the nice videos! I should try this some time. Maybe you can provide the .v files somewhere?

Nice tutorials!

I have experimented with videos too, in particular with video/slideshow hybrids. The idea is that some people don't like watching videos because they are hard to skim and navigate. Feel free to drop me a line in case you'd like to "steal" anything, I'm happy to make this open source etc.

For real math, a pen tablet works quite well; I simply copied the style of Khan Academy. The 90€ purchase is easily justified with the observation that "professional mathematicians need professional tools". I think that blackboard or paper don't work so well because the visual quality tends to be rather poor. CCD noise, compression artifacts etc. That said, it is a tad easier for me to do nice handwriting on paper.

Concerning hearing your own voice, I have found that applying an audio plugin that simulates light reverb / room ambience can help.

Ayn recommendations on a tablet (for Mac)?

Heinrich Apfelmus

I bought a Wacom Bamboo Fun. Works flawlessly with my Mac. Highly configurable, too.

Note that the Bamboo Fun has (had?) two different sizes: a smaller S version and a larger M version. (The website only shows the larger version.) I bought the smaller version, whose pen sensitive area has the size of a postcard. If I were to buy again and if I had sufficient funds, I would buy the larger version, though, because that leaves more room for handwriting.

Dan Ghica

Andrej, the tutorials are great. Can you please add one more that has some structural induction? I would like to see how you prove this:

Theorem map_id : forall ls, map id ls = ls.

Cheers! Dan

Dan Ghica

I managed to do it myself eventually. (Theorem map_id : forall ls, map id ls = ls.) It's great stuff this Coq.

Dan Ghica

... and you do have a tutorial on recursion and induction, just that it's not linked from this page. Dan.

Wiktor

Great screencast!

[...] Video tutorials for the Coq proof assistant [...]

[…] There were some things I recognized, but also a lot of things that were foreign. I found these video tutorials for Coq by Andrej Bauer, which were very helpful. I tried following along, but I didn’t get very far […]

[…] There were some things I recognized, but also a lot of things that were foreign. I found these video tutorials for Coq by Andrej Bauer, which were very helpful. I tried following along, but I didn’t get very far […]

Stephanie

Thanks a lot for the helpful videos! Without them, I couldn't have gotten started with Coq. You're doing a very nice job.

Jordan

Very nice videos. Thank you for posting!

Acrede

These tutorials are brilliant. Terse enough to keep you interested, and the examples are appropriate too. Thank you!

[…] Video Tutorials (Andrej Bauer) […]

Andrew Dabrowski

Great tutorial. One issue: I wasn't sure of the logical context from which Coq starts. Is it intuitionist logic? That might have been made clear.

How to comment on this blog: At present comments are disabled because the relevant script died. If you comment on this post on Mastodon and mention andrejbauer@mathstodon.xyz, I will gladly respond. You are also welcome to contact me directly.