The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

I think the system we're building could be effective in that context.  Our first target audience is beginning computer-science undergraduates, to whom we aim to introduce both functional programming and rigorous math and proofs.  I wouldn't naturally cover continuous math there, but probably the tools would also help with continuous stuff.

I'll certainly let you know when our public release is ready.

On 08/31/2014 05:46 PM, Vladimir Voevodsky wrote:

I am. In fact we are looking for resources which could be used for a project of the following form:

I have this idea that it would be good to:

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.

On Aug 31, 2014, at 10:15 PM, Adam Chlipala <adamc AT csail.mit.edu> wrote:

We're working on a novice-oriented interface at MIT.  I expect we'll make a public release in the next month or so.  However, you also might not be interested in a novice-oriented interface. :)

On 08/31/2014 05:13 PM, Vladimir Voevodsky wrote:

Hello,

is there a working web interface for Coq?

When I tried ProofWeb it told me 'Welcome to Coq trunk (Nov. 2006)"

and then it refused to work at all (could not start a new line after the first sentence).

Vladimir.