Thanks for posting your impressions. I'm not quite sure what to make of it all yet, but it would be interesting to hear more of what people think.
Looking at his YouTube home page, he posted 5 related videos about a month ago. His exploration of Metamath seems to start in the middle of the 2nd video. 1. "twitchcoq, writing a language we can prove things in" https://www.youtube.com/watch?v=VTFaWOPspEo (8 hrs) 2. "twitchcoq : pt 2, can we prove true is not false | Coq (software)" https://www.youtube.com/watch?v=-zf8gU0Y5WU (4 hrs) 3. "twitchcoq : pt 3, mostly I want to complain about metamath" https://www.youtube.com/watch?v=hKi9Q3S1Nsg (5+ hrs) 4. "twitchcoq pt 4, metamath says 2+2=4 | pt 5, program search" https://www.youtube.com/watch?v=OAXjsUZoOgo (7.5 hrs) 5. "obscure languages sunday : LEAN metamath parser" https://www.youtube.com/watch?v=4Or-5OLCNDA (6 hrs) I looked only at brief excerpts so far. In the second video, after playing mostly with Coq, his curiosity about Metamath seems to start at 2:27:12 when he says, "Metamath zero? What's metamath zero?" although I can't tell what he's looking at. Then from a Google search, he looks at Mario's arxiv abstract page, then the Hacker News article, and says "This might be a better base. Coq might be too complex." At 2:28:17 he starts playing David's Gource video and says "That is(?) really cool" and "Wow, Metamath's been around forever". I haven't watched the remaining 1.5 hrs. Norm On Sunday, December 22, 2019 at 8:26:30 AM UTC-5, savask wrote: > > I watched though the video and spotted a few things not mentioned in > Wolf's notes. > > At around 1:02 (1 hour 2 minutes), he starts writing a grammar file based > on the EBNF in the Metamath book. The book uses dashes inside symbols on > the left hand side of each rule, which is apparently not shared by all EBNF > standards, so he has to replace them by underscores. GNU bison supports > dashes (but calls it a GNU extension, incompatible with POSIX Yacc), Happy > parser verifier (for Haskell) also doesn't allow dashes in symbol names. > Maybe it is worthwhile replacing dashes by underscores in the Metamath book > EBNF? It may save someone time, in case if they would like to simply copy > the grammar file from the book. > > At 5:02, he tries mmj2. Apparently there's some sort of trouble launching > it on the MacOS (he had to modify the starting script), so maybe that bug > should be fixed. > > My impression is that most of his complaints come from missing > proof-assisting capabilities of the metamath program and mmj2, but main > points stand of course. Our tooling is scarce and most of work is done > manually anyway. On the other hand, the video has quite a lot of praise for > the Metamath book and the design of the language itself (stressing its > simplicity), so Metamath clearly has its strong points in comparison with > other proof systems. > -- 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/a3caf452-2cda-45ed-89c6-5416ab64c889%40googlegroups.com.
