Follow up. >> 4. Not conforming to standards. At various occasions he struggles with >> details just because they do not meet his expectations. Syntax for example
> Can you be more specific? "Not what I expect" doesn't mean it's bad. Unfortunately, this is a summary of impressions I got on various occasions, and I missed to note them down as I encountered them while watching. So I must remain short of the details. As for the 'syntax' I mentioned, it is actually a grammar describing a syntax. Doing so is a commonplace in computer science. The problem here is that the wheel is reinvented. And somebody like George Hotz knows grammars and grammar parsers well enough to understand standard grammar descriptions immediately. Instead he is forced to leap over a hurdle by adapting to a particular notation. He was able to do so, but an ideal Metamath could stay clear of such obstacles. Ok, once and for all, let me be clear here. Metamath roots back in the early 90's, and it is simply unfair to assume it is up to current standards. Norm, assembling all the details and perform their formalization was great work, and I do not want to blame anyone for the current state, which is not bad, by the way. That said, one can and should think about future directions. Wolf Lammen -- 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/8221c4d4-f3e8-4afa-88c4-8a565050e253%40googlegroups.com.
