On Nov 20, 2020, at 3:02 PM, Mario Carneiro <[email protected]> wrote: > > Relocated from > https://groups.google.com/g/metamath/c/NMZA_JRkU4U/m/ccP9bXZlAQAJ > <https://groups.google.com/g/metamath/c/NMZA_JRkU4U/m/ccP9bXZlAQAJ>: > > On Fri, Nov 20, 2020 at 9:37 AM Benoit <[email protected] > <mailto:[email protected]>> wrote: > Mario, do you have some more detail about this project to write (I'm quoting > you from github) "a verifier that would satisfy all the constraints of the CI > system in terms of capabilities: checking all the typesetting stuff, > definition checking, and full verification as efficiently as possible"? > Thanks in advance. > Benoît > > The plan is to start a new "community verifier" and build it with those tasks > in mind. I think there has been too much fragmentation in verifier land; this > makes it very hard for newcomers, especially those that are not especially > computer literate such as traditional mathematicians. mmj2 is pretty good, > but it's also quite old and the architecture isn't something I really want to > continue to build on. MM1 builds a lot of lean-esque features into a > metamath-like foundation, and I would say as a proof assistant it's a > smashing success, in usability if perhaps not in users. I've been spoiled by > lean to an extent and don't really see current metamath tools as up to par by > comparison, and building mm0-rs has been enough to convince me that it is > feasible to do the same thing for metamath. > > I value metamath's many verifiers; it's a great thing that a new verifier can > be done as an afternoon project. But a proper proof assistant needs a lot > more infrastructure to provide a high quality user experience, and the > community is small enough as it is without additional fragmentation. We've > managed to successfully collaborate on the set.mm <http://set.mm/> github > repo, but to date no verifier has received significant attention from >2 > contributors, except mmj2 which has a couple drive-by contributions beyond > the work by myself and Mel O'Cat (and I'm not actively developing the project > anymore). There is no metamath verifier I would say is in a particularly > healthy state of development.
Quick nit: I would distinguish “verifier” from “proof assistant” (as we already often do). I also value Metamath’s many verifiers. I don’t think the *verifiers* are in a bad state, they work just fine... but that’s mostly because our exceptions for verifiers are limited. It sounds like your real long-term desire is to have a “proper proof assistant”. In that case I agree with you, it would be *awesome* to have a much better proof assistant than the current options. > As a starting point, I would like to replicate the main functions of > metamath.exe, at least for one-shot tasks. That means reading and verifying a > database, but also parsing it in such a way that edits can be applied, > comments re-wrapped, and semantic information like document structure is > available. Generating the web pages would also be a target. (This is quite > difficult, as metamath.exe is a ball of hacks right now and I would like to > start from a cleaner baseline.) Sounds good. Some of the hackishness in Metamath-exe’s web page generation is because C is *terrible* at string handling. Metamath-exe is also relatively slow because it’s single threaded; if we could run the generators in parallel we could *dramatically* reduce HTML generation time. > For the more advanced tasks, one design question that comes up early is > whether to support "ungrammatical" databases. On the one hand, the metamath > spec considers such databases valid, so they can't be rejected (unless the > database contains the $j command asserting that it is grammatical). On the > other hand, grammaticality enables an asymptotically more efficient > structural storage (trees instead of strings), and also makes it possible to > perform HTML construction in a saner way, where expressions are properly > grouped rather than just appending tokens and hoping it looks well formed at > the end. (This is where a lot of the hacks in metamath.exe come from.) Note > that set.mm <http://set.mm/> and iset.mm <http://iset.mm/> are grammatical, > as well as most but not all of the smaller example databases. (I think miu.mm > <http://miu.mm/> and lof.mm <http://lof.mm/> are the main counterexamples.) > Perhaps we can degrade to a simpler verifier-only version in case the DB is > not grammatical. I think only supporting trees is quite reasonable for a proof assistant. Almost all real metamath work uses the “grammatical” databases (is there a better term?). Degrading to a “verifier-only” version is a fine long-term plan. Supporting that could even be long delayed because there are many verifiers that can already handle “non-grammatical” databases; we don’t really need another one right now. > As far as language choice goes, I would recommend Rust. Beyond being well > suited for the speed and architectural requirements of a verifier / proof > assistant, both myself and Raph Levien (if I can interest him in this > project) are involved in the rust ecosystem; maybe we can use the Druid UI > framework for the front end. (I want to put in a word of caution though: one > thing I learned from mmj2 is that it's a bad idea to write a text editor > unless that's the main goal. This is not a trivial task and will suck up all > your research time. Outsourcing the editor work for MM1 to VSCode made so > many things easier.) I agree that rewriting a text editor is a terrible idea. Reuse is vital to get things done in a reasonable time. > But really, the choice is not only up to me, as community buy-in for this > project would be important. The ultimate goal is to become the de-facto > standard proof assistant for metamath, put all our best ideas in it, and > finally get over the popular conception of metamath as not practical for real > mathematicians unless you have a high tolerance for manual labor I think that those willing to put in the effort to get started also get to pick the tech stack :-). Here are some traits I’d like to see in a better Metamath proof assistant: 1. Easily usable as a programmatic *library* from other languages. I should be able to import the library from most any other language, then use it to load databases, do queries, etc. The higher-level capabilities should implemented by calling that interface & ideally callable as well. That would make it much easier to build other things. 2. Implemented in a memory-safe language, and preferably statically typed. I like the confidence this could provide. 3. Has a small kernel implementing “legal actions”, which is distinguished from the many tactics it includes that allow trying things out without producing an invalid state as long as the tactic obeys simple static rules (the state may be *useless* but not *wrong*). 4. Support for forwards *and* backwards reasoning at least, and ideally middle-out, in its proof assistant. Some proof assistants can only go backwards; I really appreciate mmj2’s ability to do forwards, backwards, and even middle-out. 5. Lots of automation (eventually). 6. Ideally, it should include he ability to easily call out to other components written in other languages to help automation, e.g., the ability to call out to a machine learning module or some such. There are existing tools that can prove some claims; if they could be called, and then inject their proofs in a Metamath database, that’d be awesome. 7. Optional/lower importance: Perhaps enable simpler handling of parentheses within the human UI. It’d be nice to be able to use parens without surrounding each one with whitespace. I don’t think supporting precedence is important (it might even be undesirable), but it would be nice to simplify handling many parens. That may be challenging, since there are a number of constants with ( or ) in their name in set.mm such as (/) and (,). Rust is an interesting choice. It’s really easy to create a library others can call with Rust (#1), it’s memory-safe & static (#2), and it’d be easy to implement a small kernel (#3). It’s blazingly fast & easy to parallelize. If the goal is to implement something that can automatically do a lot, that’d a good start. I’ve played with Rust but not tried to build a proof assistant system with it. Would that be excessively hard? It’s true that Rust has lots of nice functional language syntactic sugar that makes some constructs easy. However, Rust doesn’t have a built-in garbage collector; its borrow system often makes that unnecessary, and that’s one reason why it plays nicely with other languages, but would we have to fight Rust too much because of that? Or is that not really an issue? Rust doesn’t natively like graphs very much (unless you disable its safeties); is that not a real problem in this case, or do alternatives such as using indices (e.g., https://smallcultfollowing.com/babysteps/blog/2015/04/06/modeling-graphs-in-rust-using-vector-indices/ <https://smallcultfollowing.com/babysteps/blog/2015/04/06/modeling-graphs-in-rust-using-vector-indices/> ) resolve that concern? One problem with Rust is that there’s no built-in REPL. If it’s accessible via an easily imported library that may be a non-problem (e.g., make it easy to import into Python and use Python’s REPL). I might be willing to help out if it’s Rust. But I have only fiddled with Rust, not used it is seriously for this kind of application, so it might be useful to hear if it’s a decent map for the purpose. To be honest, I’ve been looking for an excuse to delve further into Rust, and this might be a good excuse :-). You’ve inspired me, I think I’ll go de-rust my Rust in case this goes anywhere. However: Let’s imagine that the implementation is complete. What would interacting with it look like? What is its human UI? What is an example of a rough-draft library API? --- 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/93784378-53CE-4C6A-B057-AB837EA5388C%40dwheeler.com.
