Comment by derdi
1 day ago
Took me about 90 seconds to find a Metamath implementation bug that apparently allowed proving something that shouldn't be provable: https://github.com/metamath/metamath-exe/issues/184
1 day ago
Took me about 90 seconds to find a Metamath implementation bug that apparently allowed proving something that shouldn't be provable: https://github.com/metamath/metamath-exe/issues/184
That's with the original C verifier only. The actual database is cross-checked by 6 independent implementations. This is the whole point of Metamath: its kernel is so tiny that you can implement a verifier in a weekend.
Metamath isn't a silver bullet in the design space of formal proof tools, but I personally think it just about nails the metatheory we want. Maybe some explicit facility around definitions would be desireable.
As it happens, the Python verifier mmverify.py has an even simpler soundness bug [0], and so far I've reviewed two independent AI-written verifiers that have replicated that bug, since they apparently really like to copy the strategy from mmverify.py. A sound verifier isn't too difficult to write in terms of architecture (I just wrote one myself for differential testing [1]), but it requires some close attention to the details.
That is to say, the Swiss-cheese approach definitely lends authority, but individual implementations are unfortunately not as foolproof as they're made out to be.
[0] https://github.com/david-a-wheeler/mmverify.py/issues/30
[1] https://github.com/LegionMammal978/mm-verifier-tests/blob/ma...
Why does the original C verifier have bugs if its supposedly so easy to implement a verifier?
Ease of implementation means we get more, independent verifiers rather than trusting any particular one.
Nothing more complex than Hello world is easy to implement in C without risking mistakes in checking boundary conditions if you are not really careful.