I am going to answer to each point separately so to not let grow the text to inappropriate length.
>> 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. > Huh? There *is* a pop up showing an explanation when hovering over a name, > in both the GIF and Unicode versions. Try it out! Just go here: > http://us.metamath.org/mpegif/sqr2irr.html > and hover over any of the theorem names; you'll see the first sentence of the theorem > comment displayed. For example, step 5 uses breq2 ; just put your > mouse over that and it displays "Equality theorem for a binary relation..." > I do agree that the pop-ups are not very discoverable (if you don't know they > are there, it's not obvious to try it out). Also, hover doesn't work on most > mobile devices (touch screens generally can't hover), and mobile devices are > the most common way to view HTML pages (though they CAN detect a click-down). Yes, there is indeed a pop up. At the time I wrote those lines, I was not aware of this feature. I don't remember whether George Hotz accidently invoked one... If he did it had no effect on his opinion. I personally need no help of this kind. For one, I know the theorems in my field pretty well, and, second, if I need additional information, such as the precise form of hypotheses, I call the theorem's page directly. I more often need a search function. I use the mmtheorems' page to look for related theorems, and if nothing else helps look into set.mm directly. So we have two aspects here: George's apparent need for immediate explanation as a newbee, and my needs for a more elaborate search function. A newbee needs an overview to find her/his way through a big proof like sqr2irr. I think s/he is overwhelmed by the flurry of detail information, where important subtheorems stand indiscriminately side by side with 'glue' theorems transforming intermediate results just to link two major substeps. There is some help given by the proof indentation, other possible structuring aid at the discretion of proof creators is the use of appropriate lemmas, or explanatory remarks in the heading text. I wonder whether additional inline features like markers, frames and the like could guide through a long proof. So far, there is no way to add educational information to the proof itself, preferably added on request. My personal wish list is headed by an appropriate search function. So far I always use metamath as my primary working tool. Maybe other products like mmj2 or Milpgame feature more elaborate search functions. For a textual search in set.mm in an editor it would be helpful to have all variables appear in a fixed order, i.e. x / ph / A always appear as the first use of their kind, y / ps / B come second, and so on, so I can predict how a desired theorem looks like textually. On the web page I would like to see another link 'related theorems' next to 'nearby theorems' assembling theorems of a kind (deduction, inference, tautology, possibly more variants specializing on certain aspects). > POTENTIAL IMPROVEMENT: > Maybe there'd be a way to the hover information more discoverable > AND modify things so it's invokable in mobile devices (say by onclick). > The underlying Metamath language doesn't require short names, it's simply a > convention in set.mm, iset.mm, and many others. > We do have naming conventions, but it's fair to say that the names aren't too obvious. > I'd be fine with longer names, though I don't know if others would be. > In a few cases we have short names that perhaps could be a little longer, e.g., > "sqr" is currently short for "square root" in set.mm, but that is arguably > ambiguous with "squre"; we could use "sqrt" instead. > If we want names to be much easier to read for newcomers, though, I think > the obvious way would be to insert separators between the named parts. > The obvious separator is "_", so we could rename "sqr2irr" into "sqrt_2_irr". > We could even spell things out more fully, e.g., "squareroot_2_irrational". > Metamath tools won't have any problem with that, and compression tool > like zip will compress that to a similar size, though of course the > expanded file would be a lot bigger. > I don't know if we *should* have longer names in set.mm and friends, > but I think it's worth exploring. As for the naming conventions (I reply to Norm's related answer here as well), my first impulse is 'why not having both?'. What about alias names beside the current shorthand form (saving typing (errors)), say a descriptive display name, that is used on the web page on demand. And is found in a search instruction as well. I work as a programmer, and there is a lesson learned by professionals in this area. Use descriptive names wherever possible. It helps others understanding/ reworking your code, and the same obviously holds for proofs. As a quick introduction see https://www.geeksforgeeks.org/java-naming-conventions/. The price paid for not following these conventions in the early days of programming amounts to immense waste of working time. While the current size of Metamath with some 30000 theorems is perhaps not demanding enough for strict rules, I forsee a time where you cannot do without anymore. -- 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/08c46eac-b560-4d0d-8232-2c7f5a979e84%40googlegroups.com.
