The Coq mailing list

[George Van Treeck <treeck AT yahoo.com>]

That article brings up an important point about code (Coq proofs) still being able to work with whatever tools were used, perhaps many years from now.

And that brings to an enhancement request. I would expect Coq's "Show Proof." to show a set of unfold, apply, and rewrite statements that any mathematician could follow without knowing Coq -- instead of the gibberish it outputs now. I can not tell by looking at the current output of "Show Proof." where one tactic ends and next begins. And "Show Proof" for tactics like "auto with *", "tauto", "generalize", "destruct", etc. don't output a set of human friendly set of primitive tactics. Currently, one has to trust that whatever logic the tactic was using is correct. That is, the current output is analogous to assembler in a debugger and I'd like source code in a debugger.

-George

On Thursday, March 26, 2015 1:53 PM, Bas Spitters <b.a.w.spitters AT gmail.com> wrote:

http://math.andrej.com/2013/08/19/how-to-review-formalized-mathematics/

On Thu, Mar 26, 2015 at 5:38 AM, Pierre Courtieu
<pierre.courtieu AT gmail.com> wrote:
> Hi,
>
> The paper should imho:
>
> 1) Allow the reader to be convinced that the coq definitions do really
> model the notions you pretend. The necessary amount of sub-definitions
> needed for this depends on the number of "new" formalization layers
> you are using. For example describing extensively already
> well-established definitions/libraries is pointless (refer to the corresponding
> papers instead).
>
> 2) Allow the reader to be convinced that the final(s) theorem(s)
> statement(s) do really correspond to the one(s) you claim. This should
> be easy if 1) is OK.
>
> 3) Refer to the real Coq development, which should be put somewhere on
> the web, preferably for a long time (years).
>
> The verification task (that a referee should perform at least) is to
> download the coq files, compile them and check that the theorems are
> the same than in your paper and do really use the definitions
> described in the paper. This last step should be performed in Coq with
> commands like Print/Check/Set Prinitng All etc. Checking the files
> without running/querying Coq should not be considered enough since for
> example a small notation can drastically modify the meaning of a
> definition, without being spotted.
>
> My two cents,
> Pierre
>
> 2015-03-23 17:41 GMT+01:00 George Van Treeck <treeck AT yahoo.com>:
>> I'm a software engineer and could use some advice from real mathematicians
>> on how Coq proofs should be included with an AMS journal article.
>> I have written a article with less formal proofs for human consumption
>> paired with Coq-based proofs for machine consumption.
>> Without Coq-based proofs the paper is only 10 pages, with Coq-based about 40
>> pages.
>>
>> Being as Coq-based proofs are only intelligible at best by the Coq-literate,
>> is the normal practice to:
>>
>> a) Include long Coq-based proofs directly in article text?
>> b) Place long Coq-based proofs in an appendix?
>> c) Put a URL reference to the long Coq-based proofs in the text? If so, then
>> where on the internet should the proofs be uploaded? As *.v files?
>>
>> -George