Re: [Metamath] Re: George Hotz, a 5+ hours video complaining about Metamath, with 14000+ views and 163 thumb up
50 views
Skip to first unread message
Thierry Arnoux
Apr 12, 2020, 11:07:35 PM4/12/20
to meta...@googlegroups.com
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.
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.
Reply all
Reply to author
Forward
0 new messages