Stream: Coq users

Topic: Beginner games for Coq


view this post on Zulip Karl Palmskog (Jun 08 2020 at 10:42):

so it seems Lean+Buzzard is creating some buzz around "number games", which are essentially websites running Lean with some gamification on top, targeted towards beginners, see the interface and the source. Surely jsCoq could be used for something similar?

view this post on Zulip Donald Sebastian Leung (Jun 08 2020 at 11:51):

Speaking of websites with theorem-proving games/exercises, Codewars has quite a few of them in Coq (currently 82). In particular, 6-8 kyu exercises make for good beginner practice material IMO

(Sorry for the shameless advertisement, I couldn't resist XD)

view this post on Zulip Karl Palmskog (Jun 08 2020 at 12:01):

codewars is nice, but IMO the signup is a big barrier

view this post on Zulip Théo Zimmermann (Jun 08 2020 at 13:08):

@Donald Sebastian Leung Codewars is now advertised on the Coq website BTW (https://coq.inria.fr/documentation).

view this post on Zulip Donald Sebastian Leung (Jun 08 2020 at 13:17):

Théo Zimmermann said:

Donald Sebastian Leung Codewars is now advertised on the Coq website BTW (https://coq.inria.fr/documentation).

Thanks for your support!

view this post on Zulip Karl Palmskog (Jun 08 2020 at 13:25):

we also have Codewars listed in Awesome Coq: https://github.com/coq-community/awesome-coq

view this post on Zulip Kevin Buzzard (Jun 21 2020 at 13:47):

There is a constant stream of people (mostly mathematicians) appearing on the Lean chat saying they got interested in theorem provers because of the natural number game. I believe that there is plenty more room in this area. Here are some thoughts about what I learnt when putting this together.

view this post on Zulip jco (Jun 21 2020 at 14:33):

I probably don't have a lot that is worth cluttering the responses for, as I'm a newcomer to Coq myself coming from a CS (and functional programming) background, but I just want to say that I love your goal, and I think it's super interesting to see the mathematical perspective. I am someone for whom CS always came "more easily" than math...stuff like automata theory, complexity theory, that sort of thing all seemed to resonate much more easily than say...real analysis. But I feel like I've come full circle: now I'm getting into proof assistants (largely with CS-oriented aims), but it is making me want to learn more math. Part of that is pragmatic (to use a proof assistant, you have to do a lot of theorems, and mathematicians do a lot of theorems), but another part of it is just that...I dunno, to me, and I am probably not an outlier among this group but am an outlier among learners, math with a proof assistant is so fun! It can be frustrating when something obvious like reverse(reverse l)=l takes so long (I no joke spent about 20 hours doing that in software foundations, stubbornly not wanting to look up what I was missing and building up a massive (unnecessary, heh) series of proofs when what I really needed was just strong induction!!!!). But like, I remember picking up a book on Algebra and getting to the exercises and it's like...do I even understand what this is asking?! I think I know how to solve it, but is it correct?? With a proof assistant, you know the answer: YES. or, well, NO, as is often the case. So while my goals are more CS oriented, I'm excited to dive more into how these tools are used for more pure math

I will also say that in my time in the FP community the weird interchange regarding "what is useful math" has been interesting (and sometimes contentious?). As you highlighted, a lot of people on the CS side of things are excited by type theory of category theory...which don't even register for a ton of mathematicians.

view this post on Zulip Alexander Gryzlov (Jun 21 2020 at 14:40):

Looking through mathematician's glasses is certainly fun, however I suspect that proof assistants will at some point split into those specialized for CS and those aimed at mathematicians. This is already hinted at in e.g. https://arxiv.org/abs/2003.01491:

We believe that XTT is an ideal language for dependently typed programming, in which it is very important that coercions may be erased prior to execution (a procedure that cannot be applied to coercions arising from the univalence principle). Unfortunately, there are several obstacles rendering both OTT and XTT unsuitable for use as languages for formalizing general mathematics, disadvantages not shared by homotopy type theory or its cubical variants.

view this post on Zulip Kevin Buzzard (Jun 22 2020 at 00:22):

Ooh! Another super-important comment: the natural number game is pretty much computer-only. Any game which ran on a phone would, I believe, have far higher take-up. I think the approach we used in NNG, where some WASM trickery is used to get a javascript copy of Lean running in your browser, is doomed to failure on mobile -- but I am certainly not an expert in these matters.

The reason I think that mathematicians are an important target audience with these games is that for computer scientists, you already won. Type theory courses are normal parts of any CS syllabus (at least as far as I know -- there's certainly at least one at my uni) and theorem provers are sometimes used in these courses, and nobody bats an eyelid -- it's normal. It is vanishingly rare to see a computer proof checker being used in a maths department, the staff don't know about them so the students don't learn about them.

@Alexander Gryzlov If you're right, where will Coq go? It has made some spectacular contributions in both areas. My feeling is that there are still some very basic questions which we don't understand though, when it comes to formalising undergraduate level mathematics. I've not seen a practical working definition of manifold robust enough to be usable to do undergraduate level example sheet questions yet -- in any theorem prover. If nobody can do undergraduate example sheets, no way will the maths researchers take any of these systems seriously.

view this post on Zulip Théo Zimmermann (Jun 22 2020 at 08:27):

On behalf of the Coq developers, I can say that there is a commitment to keep supporting the use cases of the two communities (mathematicians and computer scientists). Coq is and will remain a general purpose theorem prover.

view this post on Zulip Théo Zimmermann (Jun 22 2020 at 08:30):

From what I know, this is also the case of Lean BTW: even if Lean recently became popular among mathematicians following Tom Hales' endorsement and Kevin's tremendous efforts to advertise it, the Lean developers initially wanted Lean to be a better proof assistant for verification, and I don't see why they would have forgotten about this objective.

view this post on Zulip Pierre-Marie Pédrot (Jun 22 2020 at 08:31):

This schism between CS and math proofs seems utterly artificial to me

view this post on Zulip Théo Zimmermann (Jun 22 2020 at 08:32):

It is something that comes regularly in discussions but only from the side of CS people. I believe this is due to the way the CS world is already fragmented in so many specialized ecosystems.

view this post on Zulip Pierre-Marie Pédrot (Jun 22 2020 at 08:33):

if anything, I would have suspicions around mathematicians instead (preaching for my choir...)

view this post on Zulip Théo Zimmermann (Jun 22 2020 at 08:33):

So it seems that more specialized tools are always needed and that this will result in a schism, but IMHO, specialized tools will continue to appear regularly, while mathematicians will use something that has already a large enough community...

view this post on Zulip Pierre-Marie Pédrot (Jun 22 2020 at 08:33):

I have several mathematician friends who publicly expose a despise for anything computer related

view this post on Zulip Théo Zimmermann (Jun 22 2020 at 08:34):

@Pierre-Marie Pédrot Well, that's precisely what Kevin is saying and why he's targeting so much of his efforts towards newborn mathematicians.

view this post on Zulip Pierre-Marie Pédrot (Jun 22 2020 at 08:35):

right, but then I don't see the point on insisting that this is not CS, for god sake, this is math

view this post on Zulip Pierre-Marie Pédrot (Jun 22 2020 at 08:35):

"your purity is safe"

view this post on Zulip Pierre-Marie Pédrot (Jun 22 2020 at 08:35):

a proof is a proof

view this post on Zulip Pierre-Marie Pédrot (Jun 22 2020 at 08:36):

don't mention CS and that's it

view this post on Zulip Alexander Gryzlov (Jun 22 2020 at 17:52):

Kevin Buzzard said:

Alexander Gryzlov If you're right, where will Coq go? It has made some spectacular contributions in both areas. My feeling is that there are still some very basic questions which we don't understand though, when it comes to formalising undergraduate level mathematics. I've not seen a practical working definition of manifold robust enough to be usable to do undergraduate level example sheet questions yet -- in any theorem prover. If nobody can do undergraduate example sheets, no way will the maths researchers take any of these systems seriously.

IMO, Coq won't pick a side, as stated later in this thread. However we'll probably see some specialized tools making concrete decisions about their treatment of higher equalities. This can manifest simply as different modes within a single assistant of course.

view this post on Zulip Karl Palmskog (Jun 23 2020 at 11:31):

in contrast to in math, I think it's very rare that "proofs win prizes" in CS (maybe in computational complexity?). For example, it would be absurd to say Milner got the Turing award for the SML type safety proof. Definitions are much more the "currency" in CS, and many/most proofs are long and boring.

view this post on Zulip Karl Palmskog (Jun 23 2020 at 11:38):

in fancy HoTT jargon, propositional truncation in CS doesn't typically lose you all that much of interest - an opaque existential usually suffices

view this post on Zulip Paolo Giarrusso (Jun 23 2020 at 12:33):

Typical syntactic programming language proofs are as boring as you describe, tho I expect most are not as boring as SML, but isn't that specific to PL/logic/"theory B"?

view this post on Zulip Alexander Gryzlov (Jun 23 2020 at 13:57):

Paolo G. Giarrusso said:

Typical syntactic programming language proofs are as boring as you describe, tho I expect most are not as boring as SML, but isn't that specific to PL/logic/"theory B"?

What is "theory A"? :)

view this post on Zulip Karl Palmskog (Jun 23 2020 at 13:59):

roughly corresponds to ICALP's tracks: https://easychair.org/cfp/ICALP-2020 (although I would call security etc. "Theory C")

view this post on Zulip Karl Palmskog (Jun 23 2020 at 14:02):

I think "semantic" proofs can also be boring, let's say you're proving bisimulation with some super-fancy up-to relation without reference to a PL, can still have thousands of annoying uninsightful cases

view this post on Zulip Christian Doczkal (Jun 23 2020 at 15:27):

@Alexander Gryzlov , If I'm not mistaken, the distinction dates back to the Handbook of Theoretical Computer Science which ships in two volumes:

The Handbook of Theoretical Computer Science provides professionals and students with a comprehensive overview of the main results and developments in this rapidly evolving field. Volume A covers models of computation, complexity theory, data structures, and efficient computation in many recognized subdisciplines of theoretical computer science. Volume B takes up the theory of automata and rewriting systems, the foundations of modern programming languages, and logics for program specification and verification, and presents several studies on the theoretic modeling of advanced information processing.

If someone has an older reference to this distinction (this is from 1994), I'd be happy to know.

view this post on Zulip Karl Palmskog (Jun 23 2020 at 15:40):

one distinction in practice seems to be that theory A researchers call what they do "Theoretical Computer Science", but they are not keen to extend this label to theory B (whose researchers in my experience don't insist on or mention much the TCS label). Hence, I recall seeing TCS Stack Exchange moderation removing uses of "interactive proof" for proof assistant topics, since that term is reserved (so the user claimed) for Arthur-Merlin games and the like

view this post on Zulip Alexander Gryzlov (Jun 23 2020 at 15:40):

Interesting, though I'd have probably placed automata in the complexity camp too

view this post on Zulip Karl Palmskog (Jun 23 2020 at 16:15):

this is a funny perspective on Theory B from a Theory A researcher, very apt title: https://blog.computationalcomplexity.org/2009/03/lets-congradulate-gerard-huet-who.html --- comments are also quite fun I think

view this post on Zulip Alexander Gryzlov (Jun 23 2020 at 16:32):

This also reminds me of the "Three tribes of programming" article (https://josephg.com/blog/3-tribes/).

view this post on Zulip Pierre-Marie Pédrot (Jun 23 2020 at 16:40):

I did my PhD in the middle of the creation of the IRIF laboratory, which was the merge of a theory A lab (LIAFA) and a theory B lab (PPS)

view this post on Zulip Pierre-Marie Pédrot (Jun 23 2020 at 16:40):

there was a clear border materialized by a stair, LIAFA being on the 4th floor and PPS on the 3rd

view this post on Zulip Pierre-Marie Pédrot (Jun 23 2020 at 16:41):

you could feel the physical border when walking up the stairs :nuclear:

view this post on Zulip Paolo Giarrusso (Jun 23 2020 at 16:46):

@Karl Palmskog maybe I misspoke, but with “semantics” I wasn’t thinking of bisimulation (or much about operational semantics), but rather denotational semantics or typical logical relations (even ones built on operational semantics), including realizability/saturated sets/parametricity/

view this post on Zulip Théo Zimmermann (Jun 23 2020 at 17:15):

@Pierre-Marie Pédrot It feels much more integrated nowadays. Even if the PPS spirit remains there.


Last updated: Feb 08 2023 at 23:03 UTC