> On Nov 28, 2020, at 5:23 AM, Mario Carneiro <[email protected]> wrote: > That's fair. I wasn't intending it to be based on MM1 from the beginning, but > writing a verifier from scratch is an endeavor and especially if it's mostly > me leading the charge I will want to share code with mm0-rs because it is > currently under active development. However the aim here is not to transition > to MM0 the formal system, or at least that's not my current proposal; rather > it is to adapt mm0-rs so that it can also work with metamath as the > foundation instead of MM0, which requires replacing a few foundational types > but not nearly as much as you might expect, because the basic structure of > terms is similar to MM.
If you’re willing to do that, that sounds like a great thing, and I’d be happy to help you with that. If we can adapt mm0-rs so that it works both for standard Metamath & MM0 that’d be great, and the more overlap you can find, the more it might help your PhD work too. My understanding is that this proof development system would only be able to handle “grammatical” Metamath databases like set.mm and iset.mm. However, the vast majority of Metamath work is in such databases anyway. Rust is really fast, yet safe. I would like to develop some tactics beyond what mmj2 can do, e.g., mmj2 can easily figure out the theorem/axiom to use given two expressions, but I want to be able to say “try up to 3 steps to start from step X to produce step Y”. I realize that Metamath.exe has “IMPROVE/DEPTH”, but metamath.exe wants you to work strictly backwards, & I’m looking for greater flexibility. --- David A. Wheeler -- 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/099D12D6-6A90-4931-A805-7DA593420EC6%40dwheeler.com.
