The Coq mailing list

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

Hear Hear!

On Sat, Jan 11, 2020, 11:52 AM Timothy Carstens <intoverflow AT gmail.com> 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.
>>>
>