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.
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.
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.