> > > 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! >
If there is a graphic user interface to create, it is one for kids. How creating something that would be suitable for the adolescents to initiate themselves to logic and formal mathematics? The interface should keep the most interesting intuitions in Metamath (its human-checkable algorithms of substitution mainly, its transparent management, its proximity with the formal definitions of logic) while removing the most detering features: variable substitution mostly. Along this path, natural deduction (with a context, not with a stack) would certainly be a mandatory element. -- FL -- 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/0b5c0441-d055-4655-b7d0-fefbcf2aaca8%40googlegroups.com.
