On Fri, Oct 18, 2019 at 5:00 AM Olivier Binda <[email protected]> wrote:
> I would like to start having a look at MM0. > > Because I am pretty sure that at some point I will run into some metamath > limitation for Mephistolus and I will be sorry not to have looked at what > MM0 because I would have spent a year proving Mephistolus theorems in > metamath and I will have to start anew with mm0, to gain access to some > dynamic feature or more correctness/soundness. > > BUT, so far looking at https://github.com/digama0/mm0 and > https://github.com/digama0/mm0/blob/master/mm0.md has been frustrating > for me because : > When I look at a github page/library, I expect to > > a) quickly understand what it is about > > I don't want to look at a parser grammar to understand what mm0 is all > about (I am an human and not a computer). > > I need (simple) examples to understand what mm0 expressions look like, if > you make substitutions in them like in mm, how I can work with them as a > developer > > The underlying semantics of metamath zero is based on multi-sorted first > order logic. > > well, I don't want to spend 10 hours googling what this means. > I am a regular math teacher, and in 20 years doing high level maths, I > have never ever heard of what a multi-sorted first order logic is. > Short answer: it's a very simple logical system similar to metamath. You have quantifiers (forall and exists), a fixed set of types (like "class", "wff", "set" from set.mm), and functions on those types. Please explain to regular humans what mm0 really is (the github pages are > intended to the 3 mathematicians in the world that work on this) and how a > normal developer could work with mm0 (The technical specification is > probably there ok, but we need the human explanations) > Admittedly, it's not ready for casual use yet. There is still a lot of work to be done to make it usable, and writing documentation is not my strong suit. The most important thing you should do if you want to get started is install the vscode-mm0 extension and compile or download mm0-hs. That will give you a working IDE, and then you can play with files with extension .mm0 and .mm1. You need Haskell Stack to compile mm0-hs, and VS Code to run the editor extension. I looked at the slides here : > https://www.cl.cam.ac.uk/~jrh13/spisa19/slides_07.pdf and it somehow > convinces me that I should have another look at mm0 > > I also had a peek of a computer screen with mm0 stuff in it (with axioms, > ..) in the video about x86 and this looked like understandable stuff about > what mm0 looks like for a normal user > The file I presented in the talk is https://github.com/digama0/mm0/blob/master/examples/peano.mm0 . The accompanying file https://github.com/digama0/mm0/blob/master/examples/peano.mm1 contains the proofs and shows roughly what it is like to do proofs in MM1. b) quickly understand what benefits mm0 has over mm > MM0 is designed for some very specific goals. That means that it does very well at the things it is intended for, and poor to not at all in other things. The purpose of the project is to build a self-verifying verifier, and that means that there is a strong focus on stating theorems, and having readable statements. That is, even you, with no background, should be able to read one of the example .mm0 files and get the gist of the assertions that are being made. (That's probably an exaggeration, but it would be good to find out where it can improve in this regard.) As far as differences from MM: It has an IDE, which is different from most MM IDEs. I won't claim it's the best, but it is a nice editor mode IMO. There are some technical differences in the foundations, but they aren't that important. MM0 has honest-to-goodness definitions, unlike MM which uses axioms. In MM1 you can unfold a definition by applying a theorem whose statement matches the unfolding. It also has two kinds of variables, represented by {x} and (ph) style brackets in the theorem statements. Only variables in braces can be used in binders; if you are familiar with MM you should not go wrong in thinking that wff and class variables are always in parentheses and set variables are always in braces. > Because, If I need now to start investing 6 months of my time in mm0, I > need to understand why this is important for me > I don't suggest you invest 6 months in MM0. It is alpha level stuff. It's also not meant as a replacement for MM; rather, it is a conduit for relating MM things to the rest of the world. It's too early for world domination. > Could someone give us a comparative between mm and mm0/mm1 ? > A table like this one (explaining the drawback, features) would be nice : > https://en.wikipedia.org/wiki/Comparison_of_version-control_software > That sounds like a lot of work. If you have a set of columns, I can fill the row with MM0, but I don't really know what to put on the chart. It's probably better to ask pointed questions. c) also, under what licence does mm0 work ? > All my work is public domain. Please don't be offended by this post. I really want to have a look at mm0 > but I haven't been able to, despite my many tries. It has been a real > frustrating experience, sofar. I would like that to change. > > Best regards, > Olivier > > -- > 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/e2c44b69-9719-4134-8152-86331b9319d0%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/e2c44b69-9719-4134-8152-86331b9319d0%40googlegroups.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/CAFXXJSsbPXYK_bi6zU0Gomg6k02Sf9NcM3ga588RerNxa0yUdA%40mail.gmail.com.
