The Coq mailing list

[Kinan Dak Albab <babman AT bu.edu>]

From a proof perspective, I feel like there is little value in understanding many program verification proofs (things like CompCert or soundness of type systems etc). There real importance of these proofs is that they exist, meaning that their associated theorem are indeed true. I believe this is true for most program verification and wider computer science disciplines. The intuition of why programs/algorithms/protocols are correct or why they are designed this way is much better explained through the actual program code, documentation, diagrams, examples, and so. This is why most talks rarely go deep into actual proofs, and instead focus on examples and diagrams, and sometimes very high level proof sketches.

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. It is much more important to me that the proof writing process is optimized for both writing (reducing redundancy, relying on automation and search) and automatic checking (does not take Coq forever to check). It is much more important to understand why a proof fails / a program isn't correct, which is better done by analyzing the failing proof goal, rather than the entire proof up to that point, as well as replaying the proof one step at a time and observing the proof state (in that sense the interactive piece is a lot like a debugger).

In mathematics, this is more or less generally disagreed with. Mathematical proofs have stand alone value in them, in the sense that they may show new proof techniques, help prove other theorems, or provide additional intuition. I am not an expert on mathematical proofs to either agree or disagree with this statement, but it sounds reasonable. For program verification, the pedagogical aspect will be satisfied by any Coq proofs regardless of how readable it is. Coq proofs are examples of using Coq, and can demonstrate new ways to prove things in Coq effectively (proof patterns, tactics), which others interested in proving things in Coq can learn from and re-use. Optimizing the proof engineering abstraction to retain more pedagogical or re-use value is very important, but I argue it is different from readability, at least when readability is defined by comparison to traditional pen-and-paper proofs.

-Kinan

http://cs-people.bu.edu/babman/

On Sat, Jan 11, 2020 at 10:33 AM Siddharth Bhat <siddu.druid AT gmail.com> wrote:

I'm no expert at any of what's being discussed (lean, coq, math, or theoretical CS), but I feel that as an undergrad / hopeful grad student to be, it might be a useful perspective:

I personally find that even "literate" coq / agda code is quite often unreadable, coq more so that agda. The proofs tend to feel optimised for writing, not really for reading. Much of the Comp Cert proofs which I have read are tedious. The signal is honestly lost in the noise.

I would personally find it horrible if we omitted proofs from papers because a literate file exists --- papers are written to transmit understanding, formal proofs are mostly written to be verified (as far as I can tell) These are two different goals, and no current proof system in my experiences satisfies both goals.

Also,my two cents on smooth infitesimal analysis is that it is quite hard to build. We need to build algebras of polynomial rings over the reals to obtain models of infinitesimal analysis, which is non trivial. I don't know of a coq development of this. I'd like references if it does exist

Thanks,

Siddharth

sent from my phone, please excuse any typos!

On Sat, 11 Jan, 2020, 14:47 Tadeusz Litak, <tadeusz.litak AT gmail.com> wrote:

Hi Hugo,

On 11.01.20 05:22, Hugo Herbelin wrote:
>   I've known the Types community for
> now 30 years, a community who developed Agda, Coq, Isabelle, Idris,
> Matita, Twelf, Alf, Lego, Epigram, ... a community who welcomed NuPrl,
> Mizar, PX, the QED manifesto ... a community who will also now invite
> Leo de Moura at its next conference in March in Torino. I'd be happy
> to see this collaborative spirit being prolonged. There is indeed so
> much to do in the building of proof assistants and interactive theorem
> provers, towards better foundations, towards more expressive and more
> intuitive proof languages, more robust and more expressive tactic
> programming languages and automation, more cooperative ecosystems of
> libraries (and, probably, we should find here better ways to let users
> and developers collaborate altogether).

Perhaps my comment about nobody being able to master simultaneously all available proof assistants was likely to be
misinterpreted. I never wanted to suggest that there should be just one (or two or at most three) of them on the market.

It was in reaction to the specific claim that proofs on paper became obsolete. I do not quite agree that it is enough to
say "proofs are available as source code of such-and-such proof assistant", especially in a mathematical paper. Software
rot and the Tower of Babel problem are just two example reasons why this is problematic.  The situation is made even
worse by the way conference system works, encouraging people to omit proofs from the body of the paper anyway.

Yes, it is obviously fine to omit trivial proofs, which would be anyway dismissed as "exercises for the reader", "easy
corollary", "trivial induction" etc.

It is also fine to use "literate" code in the paper, although what is "literate" for a proficient user of one proof
assistant might not necessarily be so for readers accustomed to other systems and notations. And even the syntax of each
specific proof assistant tends to change over time.

But the blunt statement that paper proofs "have outlived their usefulness" and should be omitted altogether is not the
right message to send, especially in the present state of affairs.

Best,

t.