Interesting! I think the hurdles George Hotz encountered at his first contact with Metamath are very common, especially with people with programming background.
Nowadays there are less limits in naming, e.g. the 8+3 DOS file naming is no more, same for symbols in programming languages. Actually, some of George’s complaints could be easily worked around: - Metamath already supports file inclusion, and we could very easily split set.mm into several files, in several directories, with a hierarchy. - Nothing prevents us either to use longer, more expressive names, for symbols and for theorem names, except that doubling theorem names would double the database length. -- 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/98133906-0D11-4DBA-B970-B26DACEB68E6%40gmx.net.
