Thanks for the link, Glauco. I followed this video up to 2:00:00, and had an editor open to scribble down some notes while I was watching. Here are the results. Please note, these are impressions made on the fly, and perhaps not well thought over.
1. Metamath hype: Why on earth is someone like George Hotz interested in Metamath at all? There seems to be a hype around, judging from his first words. 2. Cryptic labels: He is ranting while faced with theorem names on the HTML page of sqr2irr. No clue whatsoever what they mean. Compares this to more explicit names found in competing products, and in program code in general. I think there is indeed headroom for improvement here. Maybe a pop up showing an explanation while hovering over a name alleviates the situation. 3. No directories, just a global scope. Yes, this is a drawback in my eyes, too. But this is not an easy task as it seems at first sight. If you take this idea seriously, i.e. topics are finally independent, you end up with a need for a linker infrastructure. Compare to compiler. 4. Not conforming to standards. At various occasions he struggles with details just because they do not meet his expectations. Syntax for example 5. He somehow got lost in the gory technical details of strict proof syntax and verification. But the core idea of a Metamath proof is applying patterns to symbol strings. He seems not always be aware of this 'road map'. I remember when I first looked into Metamath I was not in the least interested in details like how variables are defined. In fact, I was not concerned with program details at all. I was satisfied to know how to replay a proof by hand. Once I learned the top level formalism, I easily could imagine a stack like structure for some automatic verification. 6 Human interface of the Metamath program. Tries out common commands at random, does not use the help feature. No GUI. 7. He feels at ease when he detects the formal syntax description of the Metamath language,and elaborates on implementing it in a Python parser. Here he is on firm grounds and starts exploring Metamath. Unfortunately, this distracts him from the core idea, in my eyes, see 5. Wolf Lammen Am Sonntag, 22. Dezember 2019 02:13:50 UTC+1 schrieb Glauco: > > I was googling for a video about Emetamath, Thierry's plugin, but I found > this recent video, that caught my attention: > > https://www.youtube.com/watch?v=hKi9Q3S1Nsg > > The title is "George Hotz | Programming | twitchcoq : pt 3, mostly I want > to complain about metamath" > > I'm having a late night "dinner", so I've not had time to understand the > whole story yet, but it looks like George (a well-known hacker, you can > read about his life on Wikipedia) has streamed and recorded a number of > multi hours videos (this is the third one) about him programming a parser > for Metamath (he read the Metamath book just before the videos). > > I've had time to look at the first few minutes, where he complains about > set.mm > > > Glauco > > -- 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/f54685dc-a6f9-4a41-bf41-f5880a67b25b%40googlegroups.com.
