On Wed, Jun 1, 2022 at 1:15 AM Jim Kingdon <[email protected]> wrote:
> 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. > It is fancy, and it is too bad that this is the case. If you recall this is one of the reasons I started working on MM0, the definition checker is way too important to be bolted on the side like it is in metamath. Mario -- 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/CAFXXJSuQ559xCk2qjneXbJqGJLFBuWghfb4iYCegafPQMp4fdA%40mail.gmail.com.
