On 5/31/22 17:34, Mario Carneiro wrote:
I don't think proliferation of verifiers is a problem at all. I would like to see metamath verifiers on Rosetta Code and written in 200 languages. It's a weekend project so it doesn't have the same risks unless you want to start adding fancy features like math parsing or markup rendering, or anything that is not just read-only on the mm file.
Hmm, by that criteria a second implementation of the definition checker would seem to be "fancy".
Which is too bad, in the sense that it is (at least to my way of thinking) part of the "kernel" in the sense of being needed to confirm soundness.
I suppose this is another case of "we won't run out of projects to work on". -- 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/78bf344d-4e44-e9b0-3812-f42e4f230c8c%40panix.com.
