The Coq mailing list

[Timothy Carstens <intoverflow AT gmail.com>]

I like this perspective. It's all about HCI. What ends are the users pursuing and how do proofs fit into those stories?

The maintenance question in particular is an interesting one.

For the software engineer tasked with maintaining an executable artifact against a stream of evolving requirements and environments, proof maintenance is going to be a pretty big deal. The proofs don't need to be particularly readable, as their main purpose is to merely exist.

For the mathematician tasked with proving new theorems, proof maintenance might be a concern in the early stages of new definitions, but at some point the goal is to have a Theorem that's been rigorously Proven and That's That. Here we care a great deal about readability, in the sense described below:

Regarding proof insight, I'd lose my math license if I didn't respond. There are rote proofs and there are insightful proofs. Rote proofs give examples of typical usage of core ideas. Insightful proofs demonstrate approaches that can be generalized to yield more theorems. The line between them is subjective and evolves over one's career. From this perspective, the value of many papers isn't the theorems they contribute, but rather, the constructions and methods they exhibit to achieve those theorems.

Such contributions won't be replaced by tactics. At least, not entirely, and not overnight. Sometimes the key step is to construct exactly the right function, the right measurable set, the right sheaf, etc, and the key contribution is a smart way of encoding some important data in this construction. The encoding schema becomes the tactic. "Ah, this ring homomorphism has a kernel whose elements are exactly the obstructions to my lemma. It also factors through this ramification, which means ..." Sometimes theorists need to build a few examples of such arguments before the general principle comes into clarity. Only then can you profitably use adages like "every algebraically closed field is C," a statement which is simultaneously false yet also shockingly insightful for certain purposes.

Calling back to my earlier reference to FRAP, this is a big reason why I'm such a fan of mechanized logic and literate proofs. In prose it's easy to sneak a ton of definitions and constructions into the statement of a lemma or its proof. This gives pretty typeset documents but also obfuscates what's going on. "Oh, I need to compute the action of this canonical map, time to go to page 127 and trace the steps of the proof of Lemma 5.12."

Compare to the situation in Coq/etc. See what happens when you bury constructions in your lemmas and proofs. You can, but it's not pretty. Best to break things up and organize it nicely - which happens to also be what the reader wants.

All my best,

-t

On Sun, Jan 12, 2020 at 9:25 AM Adam Chlipala <adamc AT csail.mit.edu> wrote:

I do think it's worth drawing a distinction between the mathematician's
goal of understanding a proof to attain "insight" (honestly driven
primarily by aesthetic criteria in many cases, as far as I can tell) and
the formal-methods engineer's goal of understanding a proof to be able
to maintain it.  We measure success very differently in these two cases,
I would claim.  Insight can be a tool to put a person in a good position
to do maintenance, but good enough automation can remove the need to
develop any insight about many details in a long proof.

On 1/12/20 11:45 AM, Stefan Monnier wrote:
>> This is why I do not really care if Coq (or lean or agda or anything
>> else's) proofs are readable or not when it comes to program verification.
> As a user of the program, that makes sense.  But if you ever intend to
> work (extend, modify, ...) on that program (or pay someone else to do
> it), then you'll need this proof to be readable, just like you need the
> code to be readable, otherwise you won't be able to update the proof to
> match the new code.