How to write correct code by construction using the Coq Proof Assistant

Also take a look at Dafny, Why3/WhyML, and Ada/SPARK. Very pragmatic tools that are getting some industry adoption.

Coq and Isabelle also see some use, but they are more costly to use in my experience.

I've done Logical Foundations and part of Programming Language Foundations, and some of the stuff in your tutorial is new to me (especially dependent types).

Your tutorial is very interesting, but in comparison to the Software Foundations series you have relatively few exercises and they're all at the end of the chapter. I found it helpful to do exercises as I went along, in many cases testing or exercising my knowledge of a new concept or Coq feature right away. So I would suggest writing more exercises and sprinkling them closer to where some of the material is introduced.

Also, some of your exercises in some chapters have a pretty steep ramp-up in difficulty, so again it might be nice to have exercises that gradually build in difficulty.

These are probably important considerations when readers are going to be working through this material entirely on their own and it might be their first exposure to Coq. (I think your tutorial says it was previously presented in-person, which has got to be a lot easier, since people can ask questions!)

Thanks for writing and sharing this material!

A cursory search reveals they're not builtin, but were written for the talk: https://github.com/awalterschulze/ccc-talk/blob/main/Coq/src...

    nail ~= intros
    wat ~= discriminate
    etc.

I used Coq in one class in school, and I never encountered wat or wreck. It’s possible they’re user- or library-defined tactics.

One thing I think is important about Coq is that it really is meant to be interactive. Even after a fair amount of usage I still find it somewhat tricky to just read a proof, especially a nontrivial one. A good IDE will show you a panel that includes all your hypothesis and requirements so far, updating as you run each line

As other people note, a lot of those seem to be local aliases defined by the author.

But the most important thing to understand about Coq is that it's meant to be read in an IDE. The IDE will show you, at each step, what has been proved and what remains to be proved. The "tactics" you see above basically mean, "At this point in the proof, we can make progress by substituting Hv. And in context, this will make sense.

But without being able to see the proof state at each step, Coq can be incredibly cryptic.

They are not built-in, no. https://github.com/awalterschulze/ccc-talk/blob/1e781326d2e3...

> I'm not sure if mathematical proof is the way to go. There's just too much code to cover for this approach to be realistic.

It may be unrealistic, but people are doing it anyway. It may be the case that there are just a few Leslie Lamports capable of doing this stuff, and it's unrealistic to expect the rest of us to.

But even if that's the case, I still want them to publish their code as libraries, so I can reach for tools that will work - even if I couldn't have proved it myself.

And if this whole mathematical/proofy way of doing things is a dead end (which I strongly disagree with - we're just at the beginning!) then it's no big deal, because we are already really good at turning JSON into stack traces.

Turning a foam architectural model into a house without the required cost investment because the foam model was “so quick to make” feels like a frustratingly accurate description.

Yep, we build a foundation with plywood and styrofoam and then someone comes and asks you to build a skyscraper on top of it.

It's a standard phrase in the formal methods field, [0] emphasising that it's an alternative to the usual approach where we hope that our testing (which can never be complete) is enough to catch all the worrisome bugs.

Personally, this article didn't strike me as being very easy to follow, or as being the most compelling demonstration of the value of formal methods. At the risk of going off-topic: if you're not seeing the point, I recommend this example using SPARK, a non-functional language. [1]

[0] https://betterprogramming.pub/a-taste-of-coq-and-correct-cod...

[1] https://docs.adacore.com/spark2014-docs/html/ug/en/tutorial....

Right, not all of the techniques shown yield code that’s correct by construction. For example, an argument was indirectly given, and that error was only found after writing a theorem involving it and finding it was impossible to prove.

In the section “Correct BST by Construction”, they explain the technique of requiring every constructor of a BST to supply a proof that it maintains the properties of a BST. Any modification to a BST constructs a new BST (since Coq is pure), so any operations on a BST must also supply a proof of their correctness. That is correct by construction.

In the general case, the "write the spec and the AI does the rest" boils down to automated theorem proving, and I'm optimistic AIs will get pretty good at this in a lot of useful situations.

Even today, in limited well-defined problem spaces, there are sometimes good algorithms for this sort of thing. See Dana Angluin's algorithm for learning the DFA that recognizes a regular language given through an interactive process of having the user provide examples/counterexamples, which serve to provide an increasingly constrained spec.

AI probably disrupts programming in the next couple of decades, where they produce not only software but static and dynamic validation artifacts of correctness. It’s sad though, I would have really liked to see how human programming could improve with better tooling, it seems like a lot of formal specification work (and program synthesis using such) could be improvised with just better user interfaces.

'dang changed it to the subtitle because it was trollish: https://news.ycombinator.com/item?id=37374404