Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Interest in Coq-based mathematics classes?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Interest in Coq-based mathematics classes?


Chronological Thread 
  • From: Pierre Courtieu <pierre.courtieu AT gmail.com>
  • To: Benjamin Werner <benjamin.werner AT polytechnique.edu>
  • Cc: Kristopher Micinski <krismicinski AT gmail.com>, Andrej Bauer <andrej.bauer AT andrej.com>, Coq Club <coq-club AT inria.fr>, Adam Chlipala <adamc AT csail.mit.edu>
  • Subject: Re: [Coq-Club] Interest in Coq-based mathematics classes?
  • Date: Tue, 18 Sep 2012 17:56:26 +0200

Hi,

Some (quite a few actually) years ago I was very impressed by this
work by Frédérique Guihot and Loïc Pottier:

http://www-sop.inria.fr/lemme/Frederique.Guilhot/

The idea was to implement the geometry program of standard french high
school (~13 years old students). (vectors, Thales and Pythagore
therorems and so).

This was done in PCoq and the magic was that a coq statement (almost
written in french) was automatically translated into an (interactive)
figure. Students could prove statement in a forward reasoning syntax
very close to literate french mathematical style.

Sadly this work did not recieve support from french education and
somehow was discontinued. But still this is the only development that
imho had a chance to reach very young students.

Regards,
Pierre Courtieu


2012/9/18 Benjamin Werner
<benjamin.werner AT polytechnique.edu>:
> If I understand correctly, Adam is thinking of taking the approach of the
> UPenn course
> to undergraduates and even freshmen, and having the students work more
> independently,
> with less TA presence.
>
> This seems challenging but very interesting. I would be happy to follow
> this and I will check
> whether I can find some other interested people on the french side.
>
> Best,
>
> Benjamin
>
>
>
> Le 17 sept. 2012 à 23:39, Kristopher Micinski a écrit :
>
> Andrej,
>
> You are aware that the university of Pennsylvania teaches a course using the
> software foundations textbook which slightly satisfies this idea? It's the
> closest thing I can think of off the top of my head. I believe Pierce has a
> talk on it, lambda the ultimate ta.
>
> On phone,
>
> Kris
>
> On Sep 17, 2012 5:32 PM, "Andrej Bauer"
> <andrej.bauer AT andrej.com>
> wrote:
>>
>> Dear Adam,
>>
>> are you aware of the ForMath project,
>> http://wiki.portal.chalmers.se/cse/pmwiki.php/ForMath/ForMath ? It
>> seems relevant to what you are talking about. See for example the math
>> classes library at http://math-classes.org. In general, formalization
>> of mathematics is a non-trivial issue.
>>
>> It would be interesting to see an experiment in teaching math through
>> a proof assistant. I think it is quite hard to do so well. It may be
>> the case that a Coq library for research-level math, or
>> "system-building" math is not appropriate for teaching. Who knows,
>> nobody has ever tried!
>>
>> With kind regards,
>>
>> Andrej
>>
>> On Mon, Sep 17, 2012 at 1:47 PM, Adam Chlipala
>> <adamc AT csail.mit.edu>
>> wrote:
>> > I'm interested in applying Coq in teaching university students
>> > mathematical
>> > subjects, including the theory underlying computing. This message is
>> > meant
>> > to get a sense of who out there is interested in collaborating to build
>> > the
>> > necessary tool support.
>> >
>> > A bit of my personal context: I teach at MIT, which has a newish
>> > initiative
>> > MITx, for running online classes, with opportunities to apply the same
>> > technology to augment traditional in-person education. Automatic
>> > grading is
>> > a central part of the approach, and one of the biggest scaling
>> > challenges
>> > has been grading assignments where students write mathematical proofs.
>> > I
>> > think Coq is the secret weapon for addressing this challenge, but I also
>> > think we need some new tool and library support to present Coq in a way
>> > that
>> > doesn't send first-year university students running and screaming. I'm
>> > doing some initial work in this direction with students, but I think
>> > this is
>> > an idea that could really benefit from a broad community effort.
>> >
>> > So, I have two primary questions to ask:
>> >
>> > 1. Would any Coq experts be interested in spending some time at MIT as
>> > postdocs or research scientists, building the support for applying Coq
>> > in
>> > early university classes relevant to computer science? Please let me
>> > know
>> > if so!
>> >
>> > 2. Could we as a community create an open platform for contributing Coq
>> > libraries relevant to different modules of different courses? A nice
>> > user
>> > interface would be crucial, and it wouldn't be any good for each
>> > university
>> > to roll its own. I would like to see a web-based interface, with bonus
>> > points (from my perspective) if it uses my language Ur/Web
>> > <http://www.impredicative.com/ur/>. :) I also feel that we need
>> > course-specific tactic libraries, to allow proofs to be written at the
>> > right
>> > levels of abstraction, without overwhelming students.
>> >
>
>



Archive powered by MHonArc 2.6.18.

Top of Page