Now that Christmas is approaching, I would love to come up with my personal wish list, that I slowly gathered over the past years. Okay, I am not going to command others here to fulfil my needs. But maybe, one or the other point has been silently pondered by others as well. So lets see whether this results in a discussion, or even, finally, something more.
1. The user interface It is common practice nowadays to separate the UI from the so called backend. The backend is responsible for carrying out commands issued by the user. The UI should present the user with an overview of his/her options, and perhaps allow focussing on particular fields of interest. Why do you want to have these separated? There are people fantastic at creating intuitive interfaces. Others are more into abstract thinking, and can provide fast and reliable libraries. Or incorporate third-party software like search engines. The current structure of set.mm has UI elements (in form of htmldef entries), theorem signatures (i.e hypotheses and statement), and proofs in one single document, which I consider not optimal. Here's an existing example, where a separation has been successfully carried out: chess! See http://www.playwitharena.de/ for a screen shot of an UI. To really play a game you still need an engine like https://stockfishchess.org/. Both UI and engine are exchangeable. If we want to go into this direction, we need to standardize the interface between frontend and backend. And before we can do that, we need to get an overview of what capabilities are requested by the users -- that are you! 2. Proof templates At least in the area where I have worked so far, I more than once encountered a situation, where I needed a specific instance out of a theorem family, that wasn't provided. The usual action to get around this deficiency was by looking out for a nearby solution and introduce otherwise unnecessary administrative proof steps. A good example is the deduction/immediate/closed form of a theorem. Wouldn't it be nice to have these forms at hand without much ado? Apart from this convenience aspect, I would really love to extend parts of FOL to arbitrary dimensions, as applies to substitution [ z / x ] [ w / y ]... , for example. The current Metamath language has no means of expressing a proof concept, or template, that contains instructions how to create a proof for a concrete theorem instance. I really miss such an abstraction layer. There are some pitfalls here to note: One should keep a compiled form of a theorem database, where all these abstract notions are collapsed into instances as needed, instead of interpreting them over and over again. C++ is an example of a computer language that follows this idea. The executable is stripped of any helper constructs the programer might have employed in his working process. Anyway, is there an idea of how to create a meta language/grammar that fits into this field? 3. Specialization The gource video from DAW shows in how many different fields of mathematics set.mm has put its foot into. These are only the traditional fields, others might want to use ZFC in future to create abstract graph structures like trees, maps. I am pretty sure, there is much more than that conceivable. For me it is time to break set.mm up into dedicated subunits. Creating a complete HTML site of all theorems is already a matter of an hour or so on my computer. Should't there be some support of specialization? Don't get me wrong here. I think this is difficult, as it needs some sort of linking process, with all kinds of conflicts lurking (link against classic or intuitionistic logic? Use theorem A or B out of different units, one using the axiom of choice, the other not?). I would love to hear from you how you see the future here. Kind regards Wolf -- 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/2b4fa3c3-f9be-4850-bf5f-7e7c5d54003c%40googlegroups.com.
