A theoretical remark, please correct me if I'm wrong: Currently, the CI runs 5(?) verifiers on the databases. Since verifiers are not overly complex, it is very unlikely that they have a "common bug" (i.e., that all have a bug which makes the same "wrong proof" be undetected). Actually, if there were a loophole in our verification process, it would be more likely to lurk in the CI software or the .yml file or the various scripts it uses.
The bug could also come from the compilers (but again, the various compilers would need to have a kind of "common bug" which is "exploited" by all the verifiers... very unlikely). Anyway, an additional assurance would come from using other compilers (in place or in addition to the ones currently used). I do not advocate doing that in the CI, which is already overkill in my opinion, but currently, the CI compiles metamath.c using gcc (Line 102 in https://github.com/metamath/set.mm/blob/develop/.github/workflows/verifiers.yml#L102). We could compile it using the certified compiler compcert (https://compcert.org/). It supports "almost all of C11" and "generates efficient code". Has anyone tried to compile metamath.c with it ? Benoît On Monday, August 29, 2022 at 9:07:53 PM UTC+2 David A. Wheeler wrote: > > > > On May 17, 2022, at 5:29 AM, Thierry Arnoux <[email protected]> wrote: > > > > Eight seconds is respectable, we should try to add this new verifier to > our set.mm CI. > > Agreed! That's faster than some other checkers we already use, so if we > just add it in parallel it shouldn't slow down the final result. > The instructions here seem clear: > https://github.com/Antony74/checkmm-ts > > Let me know of any objections to adding it to our test suite. > > We now have several checkers based on the C++ checkmm by Eric Schmidt, > so an error in the C++ version is more likely to hit other checkers. > It's already known that N-version programming (writing multiple programs > with the > same goals) are *not* necessarily independent in terms of errors. This was > shown in > a famous software engineering paper: > "Analysis of faults in an N-version software experiment" by Brilliant, > Knight, & Leveson, > IEEE Transactions on Software Engineering ( Volume: 16, Issue: 2, February > 1990) > https://ieeexplore.ieee.org/document/44387 > http://sunnyday.mit.edu/papers/nver2.pdf > Still, while the odds of detection are *less* than one would expect from > independence, it still provides us with improved evidence that the proofs > are correct... > and that's a good thing. > > --- David A. Wheeler > > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/e211ed27-5093-4c37-8c04-a6e90387ae46n%40googlegroups.com.
