> Therefore there is a risk that official Metamath site suggests a tool which performs not so good as it has to and nobody knows that.
I don't think this is a major concern, as long as we manage expectations on the landing page. Metamath and all associated tools come with no warranty, after all. I see no reason to wait for it to be perfect before making it available for use, since anything is better than nothing and users can always download another proof assistant if they decide the JS version isn't great. (And BTW: this is the case almost every time I have seen a "we put our theorem prover on the web" situation, the web prover is not actually all that great and if you want to do "real work" you will eventually want to download the tool and use it locally. But at that point the web version has already satisfied its purpose as a gateway to heavier use. This is not to say that you can't make the web prover as good or better than the offline competitors, although even with a perfect implementation there are some fundamental limitations regarding how files are read and written in a web browser that make it not quite as good as native due to the sandboxing.) On Sun, May 28, 2023 at 11:12 AM Igor Ieskov <[email protected]> wrote: > I want to add few more things to consider before suggesting metamath-lamp > as a proof assistant to start with in the first place. Not that I don't > want a tool I am developing to be present on the front page of the official > Metamath site :) But I think I have to mention what may be not so obvious > from the technical point of view: > > This is a pretty new tool, I tested it on only simple proofs and use > cases. So far it worked well for me. I do my best to cover complex > functions with unit and integration tests. But without "testing in the > field" I cannot assure that there are no bugs. And this is not a java > application when if it works on developer's computer then most probably it > will work on many other computers. It is JavaScript code running in a > browser and risks of something may go wrong for other users is higher than > in the case of a typical java application, for example. > > metamath-lamp runs completely in a browser so I will not know how often > and how successfully it is used by others. Therefore there is a risk that > official Metamath site suggests a tool which performs not so good as it has > to and nobody knows that. > > - > Igor > > On Sunday, May 28, 2023 at 11:19:01 AM UTC+2 Alexander van der Vekens > wrote: > >> Hi Igor, hi David, >> I think the current status of metamath-lamp is already very good, but not >> good enough for a beginner. So there is room for some improvements >> (especially regarding documentation, as indicated by David). >> In any case, it is a good candidate to replace the Metamath Solitaire >> Applet (does it actually work somewhere/somehow?) very soon. Maybe a >> restriction of the scope (for beginners) could help: if only propositional >> or predicate calculus (or ZF set theory) is used (this is a great >> functionality of methamath-lamp to restrict the amount of set.mm to be >> loaded and used. "Stop at exists2" would only load definitions and theorems >> for propositional or predicate calculus, "Stop at hsmex3" for ZF set >> theory), metamath-lamp may be fast and intuitive enough for a beginner. >> >> -- > 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/8f557136-b1cc-4b7f-add7-1f0ed4275280n%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/8f557136-b1cc-4b7f-add7-1f0ed4275280n%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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/CAFXXJStVLrHNxZzVofHns5Tt7ymLX9LYmA%2BbgVKuSmBvJ_%3DWQw%40mail.gmail.com.
