Coq MOOCs and educational content · Coq users

About increasing the user base. Ocaml has a nice mooc. Did anyone try to copy that to coq?

Karl Palmskog (Jun 15 2020 at 21:37):

Théo Zimmermann (Jun 16 2020 at 13:31):

I think that if somebody was willing to allocate time to creating a MOOC about Coq, @Michael Soegtrop would be happy to provide advice so that this MOOC is accessible to the engineering public that he has in mind.

Théo Zimmermann (Jun 16 2020 at 13:32):

I would be interested in running such a MOOC personally, but I have so many other things to do that it's not even something I'd put on my todo-list for later.

Karl Palmskog (Jun 16 2020 at 13:49):

Karl Palmskog (Jun 16 2020 at 13:54):

(I have personal doubts about whether the academic community should even be doing MOOCs at all, but am all for producing course materials that can be used for regular courses)

Enrico Tassi (Jun 16 2020 at 14:04):

Yves Bertot (Jun 16 2020 at 14:39):

It's hard to know if everybody that uses the word MOOC has the same thing in mind. One aspect is to gather training material that contains video material, another aspect is to gather a lot of interested people together, so that they can learn at the same time, benefit from the supervision of teaching assistants on line, but also benefit from enough collaborative rooms where they can learn from each other.
Personally, I tried to develop a video course in 2008. The material spanned over 8 hours of introductory course (cut into bits of at most 15mns) and was used by some colleagues as extra material. As a result, I received some positive feedback (especially because my colleagues complained when the course disappeared from its usual location after a few years). Unfortunately for this audience, this course was in French, but it can still be seen at this location: my video courses about Coq.

Yves Bertot (Jun 16 2020 at 14:41):

I plan to make a few more videos in the next few weeks, but the technology will be different. I will be using OBS this time, and the videos will mostly consist of sessions where I do some exercises live. I hope this can be useful.

Yves Bertot (Jun 16 2020 at 14:42):

On the subject of MOOCs, the top management at Inria has been bugging me to organize something along these lines (and to use some of their infrastructure for that).

Yves Bertot (Jun 16 2020 at 14:43):

Karl Palmskog (Jun 16 2020 at 14:57):

the most "hip" thing in educational content these days is likely to livestream when working with a proof assistant, I found Kevin Buzzard's Lean numbers game session interesting: https://www.twitch.tv/videos/647824633

Théo Zimmermann (Jun 16 2020 at 14:58):

In just over an hour (5pm UK time, 1600 UTC) I'll be playing through the natural number game https://github.com/ImperialCollegeLondon/natural_number_game live on Twitch https://www.twitch.tv/kbuzzard . Beginners welcome.

- The Xena Project (@XenaProject)

Théo Zimmermann (Jun 16 2020 at 14:59):

Kevin apparently also holds what amounts to regular "office hours" through Discord.

Karl Palmskog (Jun 16 2020 at 15:02):

the rage these days is to do "superchats" (audience paying for streamer to answer question or discuss something) - - it would be interesting if the audience asked someone to prove a theorem or verify function on the fly while streaming, not necessarily with money involved

Karl Palmskog (Jun 16 2020 at 15:09):

the ideal would be if one also records the lower-level interaction with Coq at the same time as streaming the video, along the lines of what Talia and her colleagues did: http://tlringer.github.io/pdf/analytics.pdf

Enrico Tassi (Jun 16 2020 at 15:19):

I heard a gazillion of times that silly proofs about Peano arith would bore mathematicians to death... and now I watch a mathematician teach that... I guess I understand nothing about mathematician ;-)

Karl Palmskog (Jun 16 2020 at 15:22):

I believe his audience here is math undergrads wanting to do hip stuff in Lean, so I can definitely see that Peano could go over relatively well in that particular context. Plenty of snarky stuff about CS limitations though...

Karl Palmskog (Jun 16 2020 at 15:26):

in any case, I think the CS community can be grateful to Kevin for insight into the mindsets of pure mathematicians. For example, I once talked to a pure math PhD, and tried to explain a bit about the Coq odd-order proof... Didn't go well, since in his view, Feit-Thompson wasn't much of a theorem at all, its proof was too decomposed into to many places/papers for his liking. I couldn't really get through about the concept of a formal proof at all. Kevin's outline of how proofs in math are "ordained" by their cabal of elders (not his exact words, but the gist) explains a bit of that.

Pedro Abreu (Jun 19 2020 at 02:01):

Rob Lewis (Jun 19 2020 at 09:06):

I'm not quite sure which part of the conversation I'm expected to have insight on! I think Kevin has been successful at gamifying things. Instead of writing a tutorial that's trying to teach you something he wrote a game that you try to beat. His streams have a lot of that flavor to them too. Say what you want about the approach but he's certainly found an audience for it.

Karl Palmskog (Jun 19 2020 at 09:15):

Rob Lewis (Jun 19 2020 at 09:21):

Rob Lewis (Jun 19 2020 at 09:22):

Karl Palmskog (Jun 19 2020 at 09:24):

I disagree that our list is anything like the union of papers.html + learn.html though...

Rob Lewis (Jun 19 2020 at 09:28):

The list of Lean libraries is [mathlib] plus a few projects that were published. There are no frameworks, one UI, one package/build management system, no plugins, one or two tools. There's not much to populate a list like that.

Stream: Coq users

Topic: Coq MOOCs and educational content

Bas Spitters (Jun 15 2020 at 21:23):