Somewhat off-topic, but does anyone know the reason Inria seems to have developed such a specialisation around these types of tools? I get why you'd be there today, but is there a common link/person when that started? If so, I'd love a little nudge about where to find out more.
Edit: Thanks for responses. And a warning to others: don't start following links to advisers and students in Wikipedia, it never finishes.
Working with Coq and trying to understand and use it has been a good brain stretcher for me. It's solidified my understanding of proofs to prove a bunch of simple number theory things in it, as well as creating my own types and experimenting with them.
It's a bit above my academic pay grade, so reading the documentation is always daunting, but I understand the basics. Still can't figure out how to use the notation system.
Out of genuine curiosity, does anyone know how to pronounce the name of this project? I checked the “About Coq” page on the official website, the top-level README in the project’s repository, and the project’s Wikipedia but failed to find any suggested phonetics. There also doesn’t seem to be a definitive answer on the related English Stack Exchange post I found (link: https://english.stackexchange.com/questions/435117/how-is-co...)
What is the industry or academic prevalence or level of optimism for Coq / Lean?
The release notes do not spell Xia Li-yao consistently. Which is family name, and which is given?
For Harambe?
I've never hated a piece of software with the same burning passion I reserve for Coq, but I'm happy to see they are still around releasing new way to brutalize the mind of the unprepared.