The Coq mailing list

[Tadeusz Litak <tadeusz.litak AT gmail.com>]

@Timothy: it seems then there is less disagreement between us and your position regarding paper proofs is less radical than it originally sounded, at least to me. And we share the view that "literate programming" is not quite perfect as means of communication, at least not in its present state. Siddharth expressed this well; and it also seems to me that Agda code might be somewhat easier to read for an outsider than Coq code.

I understand the view of Kinan: most proofs in software verification are of somewhat different character than most proofs in mathematical papers. I guess that this is what Adam had in mind in the words you quoted.

And I surely agree that having trivial proofs available as code is better than not having them at all, (dismissed instead with "easy induction", "exercise", "left to the reader" etc.) Indeed, in this respect at least, the availability of proof assistants has improved the situation. And  it is a pity that mathematicians, logicians etc. are not using them more intensively, at least to avoid stupid errors.

However, both learning them and actually using them can be a very time-consuming and sometimes frustrating activity. One often finds it is better for everybody involved to leave a major formalization to a student as a project. Actually, there should be more student projects of this kind in math departments; in this way, more math students could also get some non-trivial coding skills, perhaps increasing their chances to find a back-up job when things go wrong. That would also require that their teachers learn quite a bit first, at least to be able to estimate what is realistic to demand and what is not.

But then we also have the problems mentioned in my previous emails: software rot, incompatibility and unreadability. As I said, they affect even developments within one ecosystem. I already happened to have problems trying to access or run libraries or formalizations developed by other people within last 10-15 years, both in math and TCS. Indeed, even revisiting my own little formalizations or those by my students I find that I need to keep watch over what has changed in Coq 8.5, 8.6, 8.8, 8.10... so that somebody downloading them and writing "make" or "coqc" is not in for a nasty surprise. These things need to be actively maintained. Hearing how dramatically downward compatibility can break down between subsequent versions of Lean, I would be rather worried atm about developing larger libraries or formalizations in it.

*******

Incidentally, regarding the good sides and the bad sides of Lean, some time ago I found the following blog post and comments below it quite instructive:

https://jiggerwit.wordpress.com/2018/09/18/a-review-of-the-lean-theorem-prover/

(including the comment of Andreas Abel that "They say it takes 20 years to develop a proof assistant of some maturity (Coq, Isabelle, …). It is kind of reassuring for the competition that lean hasn’t reached that level in 5 years." :-)

But judging from some of the things said in this discussion, at least some points can be already obsolete?

********

And even a large body of libraries and formalizations can turn into a somewhat isolated island. I am not sure if this is still true, but 10 years ago or so one would hear that Mizar had " the largest coherent body of strictly formalized mathematics in existence", with a formalization language claiming to more-or-less mirror the language of mathematics. These days, how many people on this list have some experience with Mizar?

*******

Coming back to the issue of fighting software rot and ensuring reusability, I don't know much about actual performance of Isabelle's Archive of Formal Proofs:

https://www.isa-afp.org/

but at least the description of the concept looks very interesting to me. There is a lightweight referring process and one gets even a DBLP entry out of it (sounds perfect for a student project which perhaps wouldn't be interesting enough for ITP, IJCAR or suchlike). But most importantly, authors and Isabelle developers commit to collaborate for at least several years to ensure the code remains consistent with subsequent updates to Isabelle itself and to the archive.  And it cover both developments in software verification and in "pure" math.

What are its similarities and differences with coq-community?

Best,

t.

On 11.01.20 17:52, Timothy Carstens wrote:
> By quoting Adam I have invited much criticism of his words (or more > precisely, the message I was trying to send using his words.) I feel > obliged to clarify what I meant and defend the passage I quoted. > > The end of prosaic proofs is not the end of prosaic descriptions of > those proofs. It’s also not a new idea or even unique to mechanized > logic. > > It’s effectively what we have today already. Show me a well-cited > math paper that spells out every detail and I’ll show you a paper > that few have fully read. > > For the most part, what we’ve got today is a system where the > important or tricky proof steps are done explicitly and the rest are > waved-over, checkable only by the other 25 people on earth who are > experts in whatever niche the paper appeared in. > > I was trying to suggest that we mostly keep this tradition, except > instead of skipping proof steps, we have full proofs given in an > accompanying mechanized presentation. Now your prose can focus on > the important ideas, and your work can be checked by people who have > never met you. > > I don’t know why people are jumping to the conclusion that the prose > in these projects is forbidden from discussing proof architecture or > calling out important steps or techniques in the argument. That’s > what prose is for! > > Regarding the notion of which mechanized logic, readability of > source code, etc ... > > Let me propose that in 2020, ”literate programming” should be > understood to mean something more user-friendly than reading source > code in a text editor ;) > > There’s lots of good approaches here, both in existence today, and > possible in principle ... be creative yo! > >> On Jan 11, 2020, at 8:01 AM, Xuanrui Qi <xuanrui AT nagoya-u.jp> >> wrote: >> >>  >>> >>> I would personally find it horrible if we omitted proofs from >>> papers because a literate file exists >> >> I'd agree in principle. Even if a literate formal proof exists, I >> feel that we're obliged to at least state the high-level proof >> idea in prose. Of course, there are always some complicated but >> uninspiring proofs (e.g., many soundness proofs, proof by tedious >> but uninteresting case analysis) which I feel OK to just omit. >> >> Imagine if students go to their first, say, abstract algebra >> lecture and find that they have to learn the proofs from a >> literate Coq file. That would just be scary. Also, consider >> conferences like ITP and CPP; one would still have to submit a >> regular-length paper accompanying their formal proof. I think the >> answer is quite clear here --- formal proofs, even literate proofs, >> are not a substitute for well-written prose. >> >> Xuanrui >> >>> On Sat, 2020-01-11 at 21:02 +0530, Siddharth Bhat 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. >>>> >>