Karl Palmskog (May 18 2020 at 19:57): Karl Palmskog (May 18 2020 at 19:57):Is this supposed to be in jest, or serious? If true, I guess we can scrap most of CPP reviewing...
Step 1: The board will decide whether the theorems stated are of sufficient importance to warrant inclusion,
and
Step 2: Just run the code! If it compiles, it's right! No need for refereeing!
(Isn't that incredible???)
Source: https://twitter.com/AlexKontorovich/status/1261350127286890499 Background: https://think.taylorandfrancis.com/special_issues/interactive-theorem/
4/ Step 1: The board will decide whether the theorems stated are of sufficient importance to warrant inclusion, and Step 2: Just run the code! If it compiles, it's right! No need for refereeing! (Isn't that incredible???) Deadline for submission: Dec 31st, 2020
- Alex Kontorovich (@AlexKontorovich) Karl Palmskog (May 18 2020 at 20:24):IMO, proper ITP artifact reviewing is super tough, and should involve lots of tooling (like dependency checking, axiom tracking, mutation analysis, ...) by experienced users/developers of the system
Pierre-Marie Pédrot (May 18 2020 at 21:50):@Karl Palmskog if this is indeed real, then paper bonanza from our community! Let us never forget the one bitcoin I hard-earned by Definition False := True. :money_with_wings: :paper: :hammer:
Karl Palmskog (May 18 2020 at 22:14):Twitter account has 5000+ followers and seems consistent with https://math.rutgers.edu/~alexk --- he even gets some comment on the original tweet from Fields medalist Gowers: https://twitter.com/wtgowers/status/1261668207880011778
@agolian @AlexKontorovich I wonder whether one could speed up the process by developing corpora of "trusted results" whose correctness was not in any serious doubt and which were therefore considered fair game to use to prove other things formally. 1/
- Timothy Gowers (@wtgowers) Karl Palmskog (May 18 2020 at 22:17):he [Gowers] is seemingly not yet aware of a certain axiom-free library of what one might call "components" which one might use to "prove other things formally" --- or does he actually mean a corpus of informal math? If the latter, unclear to me how it would help...
Christian Doczkal (May 19 2020 at 08:01):Maybe someone (with more "standing" than me/us) could write one or both of them an email, inform them, and ask them to clarify what they mean?
Théo Zimmermann (May 19 2020 at 11:03):FTR there was a reply from someone in the field of ITP who explained that this reviewing process might be a bit simplistic. I just bumped the comment to the top of the replies by liking it with my own Twitter account and Coq's Twitter account.
Bas Spitters (May 19 2020 at 12:16):I've linked to ITP and CPP:
https://twitter.com/BasspittersBs/status/1262718119090495489
@AlexKontorovich @stuckintheory The formalization of (mathematical) proofs is a specialized discipline with well-established practices. Will you be following the same standards? E.g. https://popl21.sigplan.org/home/CPP-2021 https://waset.org/interactive-theorem-proving-conference-in-july-2020-in-paris
- Bas Spitters (@BasspittersBs) Karl Palmskog (May 19 2020 at 15:28):Alex cited this from the paper call in response to issues raised (https://twitter.com/AlexKontorovich/status/1261651977739665412):
Any code must be extensively documented with comments that make it readable by a professional mathematician with little formalization experience
I guess it's all fine if it's surface-level readable, i.e., no semantic exploration needed? Maxime's puzzles comes to mind...
@stuckintheory These are very good points. The call for papers explicitly states: “Any code must be extensively documented with comments that make it readable by a professional mathematician with little formalization experience” So this fact will need be to ascertained (by referees...)
- Alex Kontorovich (@AlexKontorovich) Karl Palmskog (May 19 2020 at 15:53):I still think it would be a good idea if someone with sufficient credentials/standing emailed Alex to explain why "surface level inspection" and reading comments are simply not enough (along the lines originally suggested by Christian above).
Pierre Courtieu (May 19 2020 at 16:19):Maybe linking to this:
http://math.andrej.com/2013/08/19/how-to-review-formalized-mathematics/
Would give a hint of the real work needed?
Karl Palmskog (May 19 2020 at 16:23):Assia's writeup is also good: https://project.inria.fr/coqexchange/checking-machine-checked-proofs/ and also https://proofartifacts.github.io/guidelines/
Karl Palmskog (May 19 2020 at 16:37):To be honest, this [instructions for reviewing Coq formalizations] is again something that could be crowdsourced specifically for Coq and maintained in coq-community IMO. Many people are not aware of coqchk and Print Assumptions and so on. Or perhaps it even belongs in the manual @Théo Zimmermann?
Théo Zimmermann (May 19 2020 at 16:41):Yes @Karl Palmskog, I feel like it would be a good addition to the reference manual. You may be aware that the reference manual has been completely restructured in 8.12 (cf. https://coq.github.io/doc/master/refman/). CEP#43 that introduced this change contained the following about the new "Using Coq" part:
We expect to add one or two new chapters about project management / proof engineering (including how to review a Coq formalization) in the part entitled "Using Coq".
Théo Zimmermann (May 19 2020 at 16:43):Note that there will soon be a call for crowdsourced help to improve the current state of the reference manual, including by writing new content about such topics.
Théo Zimmermann (May 19 2020 at 16:44):It could even be included in the 8.12 release if it is merged by the 8.12.0 release date (expected early July, ideally for the Coq workshop).
Théo Zimmermann (May 19 2020 at 16:46):That being said, this could be completed by a coq-community repository going more in-depth on "case studies" inspired by cases encountered in a real reviewer's life.
Last updated: Dec 05 2023 at 05:01 UTC