Sebastian Ertel (Sep 08 2022 at 20:04): Sebastian Ertel (Sep 08 2022 at 20:04):Paolo Giarrusso said:
... papers by
Gonthier's team on his major development describe this step explicitly.
Thanks again for that pointer.
Notification Bot (Sep 08 2022 at 20:04):Sebastian Ertel has marked this topic as resolved.
Karl Palmskog (Sep 08 2022 at 20:05):hm, if anyone wonders most of those papers are listed here: https://math-comp.github.io/papers.html
Paolo Giarrusso (Sep 08 2022 at 20:21):Thanks for adding the link. I was thinking especially of this quote from http://www2.tcs.ifi.lmu.de/~abel/lehre/WS07-08/CAFR/4colproof.pdf (Sec. 2, pages 3-4):
these few lines,
definition of the real numbers in file real.v (about 200 lines in total) are all that one needs to read and understand in order to ascertain that the statement below in file fourcolor.v is indeed a proof of the Four Colour Theorem: [...]
The other 60,000 or so lines of the proof can be read for insight or even entertainment, but need not be reviewed for correctness. That is the job of the the Coq proof assistant, a job for computers.
Karl Palmskog (Sep 08 2022 at 20:23):maybe a bit OT, but it's not always that "smaller" means "more understandable". For example, in PL theory, your operational semantics of a language could take a couple of hundred lines to define from scratch, and your theorem a few lines to state, but to figure out what the semantics and theorem (e.g., subject reduction) means might be a multi-day/week task
Paolo Giarrusso (Sep 08 2022 at 20:30):Of course smaller _all other things being equal_
Paolo Giarrusso (Sep 08 2022 at 20:35):I think the assumption (if you're reviewing such a proof) is that you already understand the involved maths, but you want to confirm whether the formalization gets it right. And potentially you want to double-check what elaboration did.
Karl Palmskog (Sep 08 2022 at 20:39):one document I usually recommend to Coq paper/code reviewers: https://www.ssi.gouv.fr/uploads/2014/11/anssi-requirements-on-the-use-of-coq-in-the-context-of-common-criteria-evaluations-v1.1-en.pdf ("Coq requirements in Common Criteria evaluations")
Last updated: Feb 05 2023 at 22:03 UTC