Rant about mm0...

[Olivier Binda]

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

[Mario Carneiro]

On Fri, Oct 18, 2019 at 5:00 AM Olivier Binda <olus....@gmail.com> 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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/e2c44b69-9719-4134-8152-86331b9319d0%40googlegroups.com.

[Olivier Binda]

Many thanks for your answer Mario. It helps a lot.

I'll take time later (got to go to work) to link into the links you gave.
As you say it, it looks a lot simpler (and less scary) that I was imagining.
I am not interested in an ide and won't install vscode but I'll try to write an mm0 proof-checker and have fun with building/proving some simple mm0 statements.
This should give me enough mastery to understand what mm0 is (and the content of your posts about mm0) 
(I have only used mmj2 for like 1 minute (to reproduce what was happening in the david Wheeler video) and I have still been writing code that proves mm statements for the last year)

Many thanks again (also, I am a big fan of what you and the other people in this group are doing),
Best regards
Olivier

To unsubscribe from this group and stop receiving emails from it, send an email to meta...@googlegroups.com.