jco (Jun 17 2020 at 11:48): 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!
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!
Karl Palmskog (Jun 17 2020 at 11:53):Many resources here: https://github.com/coq-community/awesome-coq
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).
jco (Jun 17 2020 at 11:54):Ah, great, that's perfect. And noted!
Last updated: Sep 26 2023 at 11:01 UTC