The Coq mailing list

[Bill Richter <richter AT math.northwestern.edu>]

   > On 08/31/2014 05:46 PM, Vladimir Voevodsky wrote:
   > 1. Make a webpage for school kids where they could register, learn
   > some basic Coq, and solve problems (in Coq).
   >
   > 2. To organize a camp where the winners (those who solved most
   > problems) could go - some with stipends and some paying money.
   >
   > 3. Have such camps also organized by other people in other countries.
   >
   > 4. Eventually to have a network which will bring talented young
   > people into math through formal proofs.

    I had some interesting experience interacting with students at the
    8th Asian Science Camp in Singapore last week that resulted, among
    other things in a poster that can be seen here:
   
https://plus.google.com/+DavidRoberts/posts/SxkdFxR3Uk4?id=6052874823364569762&oid=103404025783539237119

Vladimir, these sound like very interesting educational ideas of yours and 
the original poster!  That's great you taught school kids about ``homotopy 
and a Rubik's cube.''  I think the Rubik's cube is a great way to teach 
school kids how to multiply and divide fractions of real numbers, and of 
course the non-commutative multiplication will help with matrices.  If you 
organized a way to teach Coq to school kids, I know my son would like that, 
and I would too.  It seems there are three ingredients in teaching Coq to 
school kids:
1) computer programming
2) mathematical proofs
3) formal proofs
I would not have thought you could teach (3) without a lot of (1) and (2) 
first.  Am I wrong?  As to (1), my son and I got a lot out of Matthias 
Felleisen's group 
http://www.programbydesign.org/
which claims to be able to teach Scheme to grade- and high-schoolers.  I 
never understood how to program in any language until I read their book 
http://www.htdp.org/
which I think is accessible to school kids.  Among other things, they have a 
very nice integrated editor for writing and evaluating Scheme programs 
http://racket-lang.org/, which I think is much nicer than jedit.  I think 
they have real problems with Denotational Semantics, but it doesn't come up 
in teaching school kids.  Maybe I'm getting this wrong.  Maybe the Coq 
tactics language is so usable that we can write formal proofs without 
learning computer programs. 

-- 
Best,
Bill