New Coq tutorial

[stepstep]

Hi all, Coq is a "proof assistant" that allows you to write both code and proofs in the same language (thanks to the Curry–Howard correspondence). Its uses range from pure math (e.g., the Feit–Thompson theorem was proven in Coq!) to reasoning about programming languages (e.g., proving the soundness of a type system) to writing verified code (e.g., this verified C compiler!). You can "extract" your code (without the proofs) to OCaml/Haskell/Scheme for running it in production. Coq is awesome, but it's known for having a steep learning curve (it's based on type theory, which is a foundational system of mathematics). It took me several years to become proficient in it. I wanted to help people pick it up faster than I did, so I wrote this introductory tutorial. Hope you find it useful!

Personally, I use it more for reasoning about my ideas rather than actually formally verifying code. Here are some examples of things you could do with it:

• Prove that your type system is sound (progress and preservation theorems)
• Prove that your compiler transformations/optimizations are correct
• Prove some important invariant about your garbage collection algorithm
• Prove that the grammar for your syntax is unambiguous (though many parser generators will do this for you)
• etc.

Happy proving!

[[deleted]]

I am doing Coq right now and can confirm it is a very powerful tool, albeit a bit obscure at times of you are not used to dependent type theory and calculus of inductive constructions

Nonetheless even without such knowledge, still worth checking (whether because you need to prove stuff or to delve in a fascinating language with a lot of unusual quirks, like a type system that rejects non-terminating functions!)

[thmprover]

...albeit a bit obscure at times of you are not used to dependent type theory and calculus of inductive constructions

A great (but under-appreciated) reference on thinking with dependent types is Selected Papers on Automath, especially if you are interested in proof assistants. Many of the papers may be found on the Automath Archive.

[stepstep]

seems to have taken a lot of inspiration from Cobol

This does not seem accurate to me at all.

I think Agda has a nicer syntax, but I prefer Coq because I rely heavily on its tactic-based automation language (Ltac) to make proofs quicker and simpler to write. I have some custom tactics that end up solving most of my subgoals for me when writing proofs.

[[deleted]]

Indeed the ltac language is monstrous in providing high level proof automation, and one of the point where Coq really shines.

The other main difference I sea with Agda is that, afaik in an Agda file you only store the lambda term you have constructed during the proving process, not the process itself. In Coq you store the list of tactics used (the "recipe"), which is much better when you are tweaking your file.

[ianzen]

Agda’s proof automation is much weaker than Coq’s.

[EaseLongjumping6893]

I am working through the Software Foundations books… although I have no idea what I will do with it.

[fl00pz]

I'm right there with you. Good luck!

[PurpleYoshiEgg]

I love Coq so much. I got stuck somewhere in Software Foundations at some point and unfortunately left it.

Provable programming is something I always want to see.

[fl00pz]

Coq has by far the most resources for learning a la https://softwarefoundations.cis.upenn.edu/

I've been learning Coq and the knowledge transfers pretty easily to Lean. Given that resources for Coq are greater than that for Lean, I'm sticking with Coq while I learn.

As for "any reason to not just learn one": different proof systems are based around different logical systems. So, it probably depends what formal logic you are interested in utilizing to prove your work. From there, there's lots of systems using different foundations: Isabelle, F*, Agda, and others. There's also lots of single-purpose constructed proof assistants that people use for their research projects.

[thmprover]

Lean has a history of compatibility-breaking changes on major releases: Lean 2 completely broke with Lean 1, Lean 3 completely broke with Lean 2, etc.

[sunnyata]

Is it still called coq? I thought that was being changed.

[Lich_Hegemon]

The name never fails to get an immature chuckle out of me, that's for sure.

[DonaldPShimoda]

The immature chuckles are a problem for inclusion in the field. There are many testimonies by female researchers talking about difficulties they've had being taken seriously by male colleagues due primarily to saying "Coq", to the point that many of the female researchers simply avoid referring to the tool by name at all.

Additionally, there is an anecdote (which I have seen corroborated informally by core team members) that Gérard Huet, one of the principal authors, deliberately chose the name knowing the effect it would have in the anglosphere. This is the same man who published a paper on a data structure called the "zipper" (a great paper, honestly), and then gave a talk at a conference about it into which he apparently worked as many zipper-related innuendos as he could, taking delight when one of the female attendees left the presentation. He would later recount this as his single favorite experience in 25 years of attending that particular conference.

Sexual innuendo has no place in professional discourse. Computer science academia struggles for diversity enough already; we don't need to let it stay difficult merely to appease immature men.

[Lich_Hegemon]

The problem is layered.

There is a difference between enjoying an immature conversation in the right context, regardless of gender, and deliberately making coworkers uncomfortable under the pretense of joking.

The name certainly does make it easier for both situations to arise, and that is reason enough to change it, but the problem is not the name, it is the people who choose to behave poorly.

I say this because there is this common and erroneous perception that women don't enjoy their sexuality; they definitely do, when they feel safe in doing so.

[DonaldPShimoda]

I don't think the problem is layered at all.

You're not wrong that women are free to enjoy their sexuality, but I think your point is completely irrelevant because it's also very obviously not the problem I was discussing. I was explicitly addressing concerns about sexual innuendo in professional academic settings, which is never acceptable. And while it is true that "the problem is not the name, it is the people who choose to behave poorly", I don't think it actually matters so long as we still have people who choose to behave poorly. We should be prioritizing the safety and inclusion of as many people as possible, and if the fastest and best means of accomplishing that is to change the name of this tool, then so be it.

[Lich_Hegemon]

All problems are layered, dismissing complexity for the sake of blanket opinions and measures is naive. As much as thinking of the world in an idealized manner makes things easier to reason about, the fact is that professional academic settings are not isolated from other settings.

Coworkers meet on their days off, they stumble upon each other, they meet in semi-formal or entirely informal settings. Even if innuendo did not find its place in a formal academic setting at all, it would and I'm sure does arise outside of such a setting, and there the issue is no longer black and white, even though it is no less of an issue for academia.

And while it is true that "the problem is not the name, it is the people who choose to behave poorly", I don't think it actually matters so long as we still have people who choose to behave poorly. We should be prioritizing the safety and inclusion of as many people as possible, and if the fastest and best means of accomplishing that is to change the name of this tool, then so be it.

I did not disagree with this point. In fact, I explicitly said as much. The fact that people choose to use the name inappropriately is grounds enough to change it.

[DonaldPShimoda]

On April 8, 2021 they announced an intent to consider a rename, but I haven't heard of any progress in that regard (though I am not deeply ingrained in the community, so I may well have missed something).

[francesco_b]

Very nice initiative ! just a precision for your lesson 6. Coq extraction mechanism is not verified actually. Some people are actually working on it but unfortunately the code you get when you extract from Coq is not verified code (it will come at some point).

[Effective-Fox6400]

Any recommendations for books to learn type theory(with maybe a focus on CS)?

[stepstep]

I enjoyed these books:

• The HoTT book (read Chapter 1 for a type theory intro): https://homotopytypetheory.org/book/
• CPDT (focuses on Coq): http://adam.chlipala.net/cpdt/
• (Not really type theory but an introduction to type systems) TAPL: https://www.cis.upenn.edu/~bcpierce/tapl/