> 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/25D791E9-439D-4D1A-9C7F-ED27FD68C9C8%40dwheeler.com.
