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. 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) 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 b) quickly understand what benefits mm0 has over mm 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 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 c) also, under what licence does mm0 work ? 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.
