Stream: Coq devs & plugin devs

Topic: Hour of Code and education week


view this post on Zulip Emilio Jesús Gallego Arias (Dec 02 2021 at 15:58):

Hi folks, the call for "Organize an Hour of Code in Your Community During Computer Science Education Week, December 6-12" is out.

This is something I would really like to do "An Hour of Coq" [we need to change the name of course, so "An Hour of Proof", would anyone be interested in joining me on this?

view this post on Zulip Michael Soegtrop (Dec 02 2021 at 16:26):

Maybe as non computer scientist I can help to ensure the talk is understandable for a broad audience.

view this post on Zulip Emilio Jesús Gallego Arias (Dec 02 2021 at 18:02):

Sure, that would be great @Michael Soegtrop

view this post on Zulip Emilio Jesús Gallego Arias (Dec 02 2021 at 18:02):

I think the goal is more like to have people do a mini Coq course of one hour

view this post on Zulip Emilio Jesús Gallego Arias (Dec 02 2021 at 18:02):

with jsCoq we can do that great

view this post on Zulip Emilio Jesús Gallego Arias (Dec 02 2021 at 18:03):

so, imagine for a person that has never used Coq, what would you have that person code / proof in 1 hour

view this post on Zulip Michael Soegtrop (Dec 02 2021 at 18:12):

I think unguided hands on one can't do that much in one hour. Guided hands on, I think something like a very simple expression -> stack language compiler correctness proof, similar what @Clément Pit-Claudel showed in his Ph.D. talk today, might be feasible. One has to see how many tactics one would need for that.

view this post on Zulip Karl Palmskog (Dec 02 2021 at 18:13):

Michael Soegtrop said:

Maybe as non computer scientist I can help to ensure the talk is understandable for a broad audience.

How would you self-describe professionally? Mathematician? Engineer?

view this post on Zulip Michael Soegtrop (Dec 02 2021 at 18:14):

Education wise I am physicist and job description wise I am RF engineer/architect.

view this post on Zulip Karl Palmskog (Dec 02 2021 at 18:15):

I think unfortunately even a lot of academic computer scientists at universities are not familiar with stuff like Coq.

view this post on Zulip Karl Palmskog (Dec 02 2021 at 18:16):

I always liked Xavier's minicompiler, maybe some aspect could be brought down to an hour: https://xavierleroy.org/courses/Marktoberdorf-2009/

view this post on Zulip Michael Soegtrop (Dec 02 2021 at 18:16):

Indeed. But I think most people should be able to understand the concept of an expression language and a stack machine and I usually find the simplicity of such proofs quite impressive - I really liked the corresponding chapter in SF. And I think one can sufficiently simplify it so that it is understandable and an eye opener in one hour.

view this post on Zulip Michael Soegtrop (Dec 02 2021 at 18:17):

Yes, also have a look here: https://people.csail.mit.edu/cpitcla/thesis/relational-compilation.html.

view this post on Zulip Michael Soegtrop (Dec 02 2021 at 18:30):

@Emilio Jesús Gallego Arias , @Karl Palmskog : how do you like the idea of an expression language -> stack language compiler, maybe with a few optimizations like dropping 0+x or 1*x? If you think it makes sense, I can prepare something.

Another idea would be to demo some of @Guillaume Melquiond 's tools - this is also really impressive. One could prove a polynomial approximation with Sollya + interval + gappa and show some messed up Matlab plots and totally off numerical integrals (or function approximations for that matter) and see what Coq's answer is. Maybe as a separate track? But I guess the plotting wouldn't work in jsCoq.

view this post on Zulip Michael Soegtrop (Dec 02 2021 at 18:31):

The nice thing about coq-interval is that it does insanely complicated stuff proven correct very fast.

view this post on Zulip Emilio Jesús Gallego Arias (Dec 02 2021 at 18:31):

That may be too technical for the scope of the hour of Coq, keep in mind that people are not familiar even with logic

view this post on Zulip Emilio Jesús Gallego Arias (Dec 02 2021 at 18:31):

what do the most popular hour of code do?

view this post on Zulip Emilio Jesús Gallego Arias (Dec 02 2021 at 18:31):

we could maybe do their Coq version?

view this post on Zulip Michael Soegtrop (Dec 02 2021 at 18:32):

You mean the compiler or the math stuff or both?

view this post on Zulip Karl Palmskog (Dec 02 2021 at 18:32):

the classic example is at least some small interpreter for a (deeply embedded) language, and some metatheory lemma. The payoff for general audience is that you can see it computes and so on.

view this post on Zulip Michael Soegtrop (Dec 02 2021 at 18:34):

I am not sure such a compiler proof would be too technical. The main question is if people understand the concepts of expression evaluation and a stack machine, and I think this should be the case.

view this post on Zulip Paolo Giarrusso (Dec 02 2021 at 18:35):

I suspect people understand numeric computation better than syntax, because of what they study in high school

view this post on Zulip Michael Soegtrop (Dec 02 2021 at 18:35):

The payoff for general audience is that you can see it computes and so on.

Yes, on can see the expression computes, the compiler computes, the compiled program computes and the correctness proof.

view this post on Zulip Michael Soegtrop (Dec 02 2021 at 18:35):

So how about two tracks, a compiler track and a math track?

view this post on Zulip Karl Palmskog (Dec 02 2021 at 18:36):

if there is enough audience both are nice, I don't feel qualified to give opinion on math side though

view this post on Zulip Michael Soegtrop (Dec 02 2021 at 18:37):

Maybe we should prepare a few 5..10 minute teasers, meet and decide.

view this post on Zulip Michael Soegtrop (Dec 02 2021 at 18:38):

I could do both, the compiler and the math teaser, or just one.

Are there other ideas?

Maybe some logic riddle stuff?

view this post on Zulip Karl Palmskog (Dec 02 2021 at 18:40):

we always have the games:

view this post on Zulip Paolo Giarrusso (Dec 02 2021 at 18:42):

we're talking of https://code.org/learn / https://hourofcode.com/en/how-to ? What target age? Some of those seem for "pre-algebra" — so young that symbolic computation is too abstract

view this post on Zulip Paolo Giarrusso (Dec 02 2021 at 18:43):

but I guess you'd focus on high school students?

view this post on Zulip Paolo Giarrusso (Dec 02 2021 at 18:45):

(and even then, I've seen both students and experienced programmers struggle a lot with the idea of inductives / ASTs)

view this post on Zulip Emilio Jesús Gallego Arias (Dec 02 2021 at 18:47):

That's a good question @Paolo Giarrusso

view this post on Zulip Michael Soegtrop (Dec 02 2021 at 18:50):

Ah yes, I should have looked more closely - I assumed this was for students. Very different then ...

When my son was in 4th grade elementary school, I had some interesting discussions with him if the laws of integer arithmetic are naturally as they are, or if it has been defined to be like this. Essentially his question was if e.g. distributive law is an axiom or a theorem. It ended up in some Coq demos ...

view this post on Zulip Emilio Jesús Gallego Arias (Dec 02 2021 at 18:50):

Maybe some basic math would be more interesting? The audience is for us to choose

view this post on Zulip Emilio Jesús Gallego Arias (Dec 02 2021 at 18:51):

but the idea is to have a low barrier

view this post on Zulip Emilio Jesús Gallego Arias (Dec 02 2021 at 18:51):

so a math theorem that may be at reach of anybody with a completed high school education on sciences

view this post on Zulip Emilio Jesús Gallego Arias (Dec 02 2021 at 18:51):

could be a good point

view this post on Zulip Michael Soegtrop (Dec 02 2021 at 18:52):

You mean something like sqrt(2) is not in Q?

view this post on Zulip Emilio Jesús Gallego Arias (Dec 02 2021 at 18:53):

That could be interesting? Or maybe associativity and communicativity of some operator?

view this post on Zulip Emilio Jesús Gallego Arias (Dec 02 2021 at 18:54):

Not sure, we got many good ideas, so maybe we could setup a few , and let the person choose; the main point of the hour of code

view this post on Zulip Emilio Jesús Gallego Arias (Dec 02 2021 at 18:54):

is to break the barrier of trying a tool

view this post on Zulip Emilio Jesús Gallego Arias (Dec 02 2021 at 18:54):

so before you are like "oh Coq this is black magic" and after one hour you say "oh Coq, I did something!"

view this post on Zulip Paolo Giarrusso (Dec 02 2021 at 18:55):

one maybe nice thing about Michael's "interval" idea is that high school people do lots of "computation" (by hand), like in a Computer Algebra System (does Coq qualify?)

view this post on Zulip Paolo Giarrusso (Dec 02 2021 at 18:56):

OTOH, "can a high school student follow a proof on paper" seems much more dicey

view this post on Zulip Emilio Jesús Gallego Arias (Dec 02 2021 at 18:57):

If the proof is just rewrite maybe

view this post on Zulip Paolo Giarrusso (Dec 02 2021 at 18:59):

there's also a difference between "all high school students" vs "the ones who are good at maths", and aiming for all could be nicer but unrealistic (the How to Design Programs people aim for all, but it's LOTS of work)

view this post on Zulip Michael Soegtrop (Dec 02 2021 at 18:59):

What I don't understand - are these interactive one time lessons or recorded lectures?

view this post on Zulip Michael Soegtrop (Dec 02 2021 at 19:01):

Btw.: another idea which might be interesting: you know these puzzles where you shift around 15 pieces on a 4x4 grid and you are supposed to bring them in order? If one swaps two pieces, it can't be solved any more - it might be nice prove that a certain initial configuration is not solvable (which is not hard by invariants).

view this post on Zulip Michael Soegtrop (Dec 02 2021 at 19:03):

So how about the 5 minutes teaser idea?

view this post on Zulip Paolo Giarrusso (Dec 02 2021 at 19:04):

@Emilio Jesús Gallego Arias is the call for creating new hours or running the existing ones, or are you thinking of a separate event along the same lines? https://www.acm.org/articles/bulletins/2021/december/hour-of-code-2021 seems for running the existing ones

view this post on Zulip Alexander Gryzlov (Dec 02 2021 at 19:06):

I still don't really get who's the intended audience for this

view this post on Zulip Alexander Gryzlov (Dec 02 2021 at 19:08):

Is https://hourofcode.com/ the original initiative?

view this post on Zulip Alexander Gryzlov (Dec 02 2021 at 19:10):

Anyone, anywhere can organize an Hour of Code event, and anyone from ages 4 to 104 can try the one-hour tutorials

Ok, so there are basically no assumptions whatsoever about the audience background, in that case it might be really tough to sell formal verification in 1 hour

view this post on Zulip Paolo Giarrusso (Dec 02 2021 at 19:16):

https://hourofcode.com/de/en/learn has activities for "Grades 9+" (>=15 years old?)

view this post on Zulip Paolo Giarrusso (Dec 02 2021 at 19:16):

and https://hourofcode.com/de/activity-guidelines seems the actual call for activities?

view this post on Zulip Paolo Giarrusso (Dec 02 2021 at 19:16):

After reading the guidelines, you can submit your activity through our Hour of Code™ Activity Submission page. You can submit an activity at any time, but the deadline for inclusion in any given calendar year is October 1. (For example, any activities received after October 1, 2021 will not be listed for 2021's Hour of Code.) The deadline to submit for an early qualitative review (details below) is August 16.

view this post on Zulip Paolo Giarrusso (Dec 02 2021 at 19:18):

sorry, https://hourofcode.com/en/activity-guidelines

view this post on Zulip Michael Soegtrop (Dec 02 2021 at 20:02):

So I guess we should plan for next year - which has the advantage that we can do it properly.

view this post on Zulip Paolo Giarrusso (Dec 02 2021 at 20:37):

Do notice the "early review" suggestion

view this post on Zulip Théo Zimmermann (Dec 03 2021 at 09:45):

I have just skimmed over the discussion, but FWIW, @Yves Bertot has prepared some interesting Coq demos at https://github.com/ybertot/osxp_demos_coq


Last updated: Feb 06 2023 at 19:03 UTC