coq-community / bertrand Goto Github PK

My testing while setting up CI for this repository shows that this project is not currently compatible with Coq 8.8 and above (see https://travis-ci.com/Zimmi48/bertrand/builds/78357211).

Hi @Zimmi48: I updated "bertrand" to 8.9 and 8.10 and pushed corresponding tags v8.9.0 and v8.10.0.

I did not create/update an opam package for compilation with 8.9 and 8.10. There is an opam template in the archive which I could use, but I lost track of whom is supposed to be in charge of it (the opam file says it is @palmskog but the header of the repository says it is @herbelin).

The Why program (Knuth.mlw) is unfortunately out of date with respect to recent releases of the Why toolchain; there is a modern Why program version available that is, however, "less verified" than the program here. One way to solve this, and verify fully down to assembly level, would be to convert Knuth.mlw to C and use VST, bringing the program, its semantics, and the proof all fully into Coq. Such a conversion is not easy, so I will simply leave it here as a cool idea.

The first part of this project, the proof of Bertrand's postulate, is a generic result about primes, and could be useful to a larger audience. One way to accomplish this is to have the proof transferred into the CoqPrime project, which is in the Coq Platform and has regular releases compatible with the latest released version of Coq. However, this may require reorganization and adaptation to CoqPrime idioms.

After a tentative transfer, the project here could focus fully on providing verified programs that use Bertrand's postulate (on top of CoqPrime), both using the Why toolchain and using other means. Such programs and proofs are likely to have a much smaller audience, but are still very valuable to the community.