Stream: Coq users

Topic: Resources for getting better at proofs in Coq

view this post on Zulip jco (Jun 17 2020 at 11:48):

I've done a little googling but didn't find anything conclusive. I'm a professional programmer getting into proof assistants (with an aim to use dependently typed languages in industry). So my programming background is decent, but my math background is, well, certainly not PhD at Penn level :P I'm working through software foundations (almost done with verified functional algorithms, thanks to some help here!), and I find that I can follow along, but some of the details about how to tackle proofs are beyond me (for example, I did not realize fold_rec_bis existed!). I'm wondering if there are any resources that just...sort of use coq to prove things in a lot of different areas, to help one get experience with how to use coq to prove different sorts of things, the different types of proof techniques there are, etc? Sort of like software foundations, but I guess with more of an aim on how to use coq to prove different kinds of things, rather than software foundations which is more focused on coq and, well, the foundations of software. Not sure if this is a weird thing to want!

view this post on Zulip jco (Jun 17 2020 at 11:49):

I think it'd just be nice to see more proof techniques, more applications to different types of code, so that when novel stuff comes up (like fold, lol...) I won't be as lost!

view this post on Zulip Karl Palmskog (Jun 17 2020 at 11:53):

Many resources here:

For long-form questions, we really recommend the Discourse, which is certainly not dead, although experts read it asynchronously (i.e., in their own time). One key reason for recommending the Discourse is that answers become searchable and browsable (more visible in general).

view this post on Zulip jco (Jun 17 2020 at 11:54):

Ah, great, that's perfect. And noted!

Last updated: Jan 27 2023 at 00:03 UTC