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?
Maybe as non computer scientist I can help to ensure the talk is understandable for a broad audience.
Sure, that would be great @Michael Soegtrop
I think the goal is more like to have people do a mini Coq course of one hour
with jsCoq we can do that great
so, imagine for a person that has never used Coq, what would you have that person code / proof in 1 hour
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.
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?
Education wise I am physicist and job description wise I am RF engineer/architect.
I think unfortunately even a lot of academic computer scientists at universities are not familiar with stuff like Coq.
I always liked Xavier's minicompiler, maybe some aspect could be brought down to an hour: https://xavierleroy.org/courses/Marktoberdorf-2009/
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.
Yes, also have a look here: https://people.csail.mit.edu/cpitcla/thesis/relational-compilation.html.
@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.
The nice thing about coq-interval is that it does insanely complicated stuff proven correct very fast.
That may be too technical for the scope of the hour of Coq, keep in mind that people are not familiar even with logic
what do the most popular hour of code do?
we could maybe do their Coq version?
You mean the compiler or the math stuff or both?
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.
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.
I suspect people understand numeric computation better than syntax, because of what they study in high school
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.
So how about two tracks, a compiler track and a math track?
if there is enough audience both are nice, I don't feel qualified to give opinion on math side though
Maybe we should prepare a few 5..10 minute teasers, meet and decide.
I could do both, the compiler and the math teaser, or just one.
Are there other ideas?
Maybe some logic riddle stuff?
we always have the games:
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
but I guess you'd focus on high school students?
(and even then, I've seen both students and experienced programmers struggle a lot with the idea of inductives / ASTs)
That's a good question @Paolo Giarrusso
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 ...
Maybe some basic math would be more interesting? The audience is for us to choose
but the idea is to have a low barrier
so a math theorem that may be at reach of anybody with a completed high school education on sciences
could be a good point
You mean something like sqrt(2) is not in Q?
That could be interesting? Or maybe associativity and communicativity of some operator?
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
is to break the barrier of trying a tool
so before you are like "oh Coq this is black magic" and after one hour you say "oh Coq, I did something!"
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?)
OTOH, "can a high school student follow a proof on paper" seems much more dicey
If the proof is just rewrite maybe
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)
What I don't understand - are these interactive one time lessons or recorded lectures?
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).
So how about the 5 minutes teaser idea?
@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
I still don't really get who's the intended audience for this
Is https://hourofcode.com/ the original initiative?
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
https://hourofcode.com/de/en/learn has activities for "Grades 9+" (>=15 years old?)
and https://hourofcode.com/de/activity-guidelines seems the actual call for activities?
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.
sorry, https://hourofcode.com/en/activity-guidelines
So I guess we should plan for next year - which has the advantage that we can do it properly.
Do notice the "early review" suggestion
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