The Coq mailing list

[Christophe Bal <projetmbc AT gmail.com>]

Hello.

Have you some documents about your courses to share with us?

2014-09-02 16:27 GMT+02:00 Kevin Sullivan <sullivan.kevinj AT gmail.com>:

I've now taught Coq to undergraduates -- most recently including this semester to third/fourth year students. The class has been successful. Many of the best students find the material fascinating. I'm happy to see a burgeoning effort in this area, and would be happy to contribute. --KS

On Tue, Sep 2, 2014 at 10:23 AM, Bill Richter <richter AT math.northwestern.edu> wrote:

   > 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