I'm sure you meant to say, "this is one of the reasons Raph started working on Ghilbert, then I shamelessly copied that approach for MM0."
:) R On Tue, May 31, 2022 at 10:19 PM Mario Carneiro <[email protected]> wrote: > > > 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 > <https://groups.google.com/d/msgid/metamath/CAFXXJSuQ559xCk2qjneXbJqGJLFBuWghfb4iYCegafPQMp4fdA%40mail.gmail.com?utm_medium=email&utm_source=footer> > . > -- 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/CADBEgNM2sdok8CQ4o6DGdAgM%2BNPEmrN7nXz%3DhGdd_Fjr14FgTg%40mail.gmail.com.
