Emilio Jesús Gallego Arias (Dec 02 2021 at 15:58): 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?
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.
Emilio Jesús Gallego Arias (Dec 02 2021 at 18:02):Sure, that would be great @Michael Soegtrop
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
Emilio Jesús Gallego Arias (Dec 02 2021 at 18:02):with jsCoq we can do that great
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
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.
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?
Michael Soegtrop (Dec 02 2021 at 18:14):Education wise I am physicist and job description wise I am RF engineer/architect.
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.
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/
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.
Michael Soegtrop (Dec 02 2021 at 18:17):Yes, also have a look here: https://people.csail.mit.edu/cpitcla/thesis/relational-compilation.html.
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.
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.
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
Emilio Jesús Gallego Arias (Dec 02 2021 at 18:31):what do the most popular hour of code do?
Emilio Jesús Gallego Arias (Dec 02 2021 at 18:31):we could maybe do their Coq version?
Michael Soegtrop (Dec 02 2021 at 18:32):You mean the compiler or the math stuff or both?
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.
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.
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
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.
Michael Soegtrop (Dec 02 2021 at 18:35):So how about two tracks, a compiler track and a math track?
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
Michael Soegtrop (Dec 02 2021 at 18:37):Maybe we should prepare a few 5..10 minute teasers, meet and decide.
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?
Karl Palmskog (Dec 02 2021 at 18:40):we always have the games:
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
Paolo Giarrusso (Dec 02 2021 at 18:43):but I guess you'd focus on high school students?
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)
Emilio Jesús Gallego Arias (Dec 02 2021 at 18:47):That's a good question @Paolo Giarrusso
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 ...
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
Emilio Jesús Gallego Arias (Dec 02 2021 at 18:51):but the idea is to have a low barrier
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
Emilio Jesús Gallego Arias (Dec 02 2021 at 18:51):could be a good point
Michael Soegtrop (Dec 02 2021 at 18:52):You mean something like sqrt(2) is not in Q?
Emilio Jesús Gallego Arias (Dec 02 2021 at 18:53):That could be interesting? Or maybe associativity and communicativity of some operator?
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
Emilio Jesús Gallego Arias (Dec 02 2021 at 18:54):is to break the barrier of trying a tool
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!"
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?)
Paolo Giarrusso (Dec 02 2021 at 18:56):OTOH, "can a high school student follow a proof on paper" seems much more dicey
Emilio Jesús Gallego Arias (Dec 02 2021 at 18:57):If the proof is just rewrite maybe
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)
Michael Soegtrop (Dec 02 2021 at 18:59):What I don't understand - are these interactive one time lessons or recorded lectures?
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).
Michael Soegtrop (Dec 02 2021 at 19:03):So how about the 5 minutes teaser idea?
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
Alexander Gryzlov (Dec 02 2021 at 19:06):I still don't really get who's the intended audience for this
Alexander Gryzlov (Dec 02 2021 at 19:08):Is https://hourofcode.com/ the original initiative?
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
Paolo Giarrusso (Dec 02 2021 at 19:16):https://hourofcode.com/de/en/learn has activities for "Grades 9+" (>=15 years old?)
Paolo Giarrusso (Dec 02 2021 at 19:16):and https://hourofcode.com/de/activity-guidelines seems the actual call for activities?
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.
Paolo Giarrusso (Dec 02 2021 at 19:18):sorry, https://hourofcode.com/en/activity-guidelines
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.
Paolo Giarrusso (Dec 02 2021 at 20:37):Do notice the "early review" suggestion
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: Jun 08 2023 at 04:01 UTC