Comment by mcguire | Hacker News Reader

Comment by mcguire | Hacker News Reader

And this...

"To give you an idea of what an actual proof looks like in Coq, below is a proof of one of the easier lemmas above. The proof is virtually impossible to read without stepping through it interactively, so don’t worry if it doesn’t make any sense to you here."

is why Coq is not one of my favorite tools.

A proof consists of two things: the "proof state"---a statement of what you know at a given point--and a sequence of "proof operations"---the manipaulations that move from one proof state to the next.

Most mathematical proofs you have ever seen have been presented as a list of proof states, with the operations either explained in comments or taken to be obvious.

Coq (and most other similar systems) present the proof as a sequence of proof operations, with the state invisible unless you're going through it in a Coq IDE.

On one hand, that's the same thing as a program: a Coq proof is a program for creating the proof. Unfortunately, on the other, I've never been able to read Coq proofs the way I can read programs. Probably a lack of experience, I guess.

On the other hand, Coq is a damn fun computer game.

> Unfortunately, on the other, I've never been able to read Coq proofs the way I can read programs. Probably a lack of experience, I guess.

I don't think it's a lack of experience on your part. I worked with some people at MIT who were far better at Coq than I was, and they admitted the same thing. Coq proofs are unreadable, even when all the hypotheses and variables are given thoughtful names.

But, as you found, Coq proofs are not meant to be read; they are meant to be stepped through. I'm not sure if there is really a better alternative: if the formal proofs were made easier to read, they'd probably be much longer. And they can already get quite long compared to traditional paper proofs.

I think the right strategy is to break large developments into small lemmas, such that each proof is short and borderline obvious (similar to structuring a computer program to be self-documenting). Also, more experienced Coq users heavily invest in proof automation (building "tactics" in Coq) to make proofs short and sweet. I don't have much experience on that front, though.

I worked with Adam one summer before he had that coq textbook, he’s definitely a wizard of proof automation in coq. I only much more recently learned how ltac case expressions also backtrack!

For the benefit of people without specific knowledge of people at MIT: Adam is Adam Chlipala http://adam.chlipala.net/

Is that partially a tooling problem, i.e. would it help or even be possible to show those intermediate “proof states” (as used by the grandparent) live in the IDE while you type?

Stepping through the proofs in the IDE is the only way to understand them. But that is like stepping through a program in a debugger---it's inefficient if you have a lot to understand.

Unfortunately, smart tactics make proofs even harder to read. :-)

It sounds like a similar difficulty to reading Forth, and you're proposing a solution like what Forth programmers do. I can't help wondering if we can't make up a more readable language instead.

I you prefer readable proofs, try Isabelle or Lean.

Or TLA+.

Lamport's structured proofs... should be easier. But I haven't had enough experience to say.

You can certainly do readable proofs in Coq the way you would do them in Isabelle, but this requires stating intermediate states explicitly (with assert e.g.) and Coq users rarely do that (mainly because readability is not their goal, I guess).

Are there languages that model proofs as pure functions? I.e. instead of modifying some implicit state, you pass existing proofs as arguments to other proofs that define these existing proofs as assumptions to itself.

So, a proof would be a pure function, taking a number of assumptions as arguments, and in order to write this proof you must first pass proofs of the assumptions to it as arguments (and then you can reference these proven assumptions in the body of the proof when needed).

Couldn't it be possible to unfold a proof by printing all the subsequent proof states one after the other? Wouldn't that be easier to follow?

What is your favorite tool? Agda? I've been finding it much nicer to work with, but the ecosystem is just not there yet.

Reply on news.ycombinator.com