Paolo Giarrusso said:

... papers by

Gonthier's team on his major development describe this step explicitly.

Thanks again for that pointer.

Sebastian Ertel has marked this topic as resolved.

hm, if anyone wonders most of those papers are listed here: https://math-comp.github.io/papers.html

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.

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

Of course smaller _all other things being equal_

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.

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