Stream: Coq users

Topic: Coq MOOCs and educational content


view this post on Zulip Bas Spitters (Jun 15 2020 at 21:23):

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

view this post on Zulip Karl Palmskog (Jun 15 2020 at 21:37):

I guess the obvious choice of MOOC focus would be SF

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Jun 16 2020 at 13:49):

this could be relevant as well (database of formal methods courses): https://fme-teaching.github.io/#fm-courses

view this post on Zulip 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)

view this post on Zulip Enrico Tassi (Jun 16 2020 at 14:04):

CC @Yves Bertot

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip Yves Bertot (Jun 16 2020 at 14:43):

erratum, my previous video course in French was actually in 2009.

view this post on Zulip 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

view this post on Zulip Théo Zimmermann (Jun 16 2020 at 14:58):

Ah ah, I was just writing about that and digging up the related tweet: https://twitter.com/XenaProject/status/1271094301062283266

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)

view this post on Zulip Théo Zimmermann (Jun 16 2020 at 14:59):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Enrico Tassi (Jun 16 2020 at 15:19):

Karl Palmskog said:

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

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 ;-)

view this post on Zulip Karl Palmskog (Jun 16 2020 at 15:22):

Enrico Tassi said:

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 ;-)

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...

view this post on Zulip 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.

view this post on Zulip Pedro Abreu (Jun 19 2020 at 02:01):

maybe @Rob Lewis can give us some more insight on this

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Jun 19 2020 at 09:15):

I'll take the opportunity to ask @Rob Lewis if/when you're going to make a "one-stop-shop" Lean resource/project list like this: https://github.com/coq-community/awesome-coq (getting it listed at https://github.com/sindresorhus/awesome was a real challenge)

view this post on Zulip Rob Lewis (Jun 19 2020 at 09:21):

We had something like that on our website at some point but it might have gotten lost when the website was redesigned? The mathlib repo + https://leanprover-community.github.io/papers.html + https://leanprover-community.github.io/learn.html pretty much covers it.

view this post on Zulip Rob Lewis (Jun 19 2020 at 09:22):

I'll investigate where that page went...

view this post on Zulip Karl Palmskog (Jun 19 2020 at 09:24):

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

view this post on Zulip 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.


Last updated: Jan 29 2023 at 06:02 UTC