Thanks Mario, that's definitely on my radar now! As is learning some Rust, eventually.
I tend to see WASM as a way of making use of pre-existing code, and TypeScript tends to be my preferred language for writing new code (leaving behind 20 years of C++ after gradually completing the switch), but I know there's great people doing new work with WASM too. Until metamath-knife achieves world domination, I believe there's still value in both approaches. My initial plan for metamath.wasm would be to do a version of the html proof explorer as a Single Page App. This would make the transition navigating between proofs almost instantaneous, because a copy of metamath running in the browser could generate html much faster than it can be downloaded from an external server. This would provide both a quick-win in terms of demonstrating value, and a handy proof-picking component to launch subsequent experiments from. After that, my interest is in drag-and-drop proof assistants like QED ( https://www.math.ucla.edu/~tao/QED/QED.html) and the Incredible Proof Machine (https://incredible.pm), both of which are just educational toys compared to the mathematics that has been achieved with Metamath. Best regards, Antony On Thu, Sep 30, 2021 at 12:30 PM Mario Carneiro <[email protected]> wrote: > Running in the browser is one of the goals for the (budding) > metamath-knife community verifier / proof assistant: > https://github.com/david-a-wheeler/metamath-knife/ . It's written in > Rust, and I have had success in the past compiling Rust projects to WASM, > but the web frontend for metamath-knife has not yet been written. IIRC > there was a prototype of smm3 in the browser, which can probably be lightly > adapted to get mm-knife working too. If you are interested in pursuing > this, I would encourage you to redirect your efforts to mm-knife instead. > It also has a permissive license (MIT/Apache instead of GPL v2+ for > metamath.exe), which was brought up on the reddit thread. > > Mario > > On Thu, Sep 30, 2021 at 7:05 AM Antony Bartlett <[email protected]> wrote: > >> Hi, >> >> I don't know if anyone else has tried this, but I think it may be of >> interest to a few people here that I'm making an (ongoing) effort to build >> Metamath for the WebAssembly (WASM) platform. >> >> The goal is to be able to use Metamath's functionality in dynamic >> JavaScript web-pages. Obviously proof validation is readily available for >> most major programming languages, and it's not *that* hard to write one's >> own prover, but some Metamath's richer functionality can't be found >> anywhere else (except maybe mmj2), at least until there is a community >> verifier, as has also been mooted here. I've particularly got my eye on >> html generation, and the unification algorithm. >> >> Usually I'd prefer to report only my successes, but, well, as you'll see >> from the following two posts linked below, I have been asking for help: >> >> >> https://www.reddit.com/r/WebAssembly/comments/pvye5u/porting_command_line_program_to_wasm_and/ >> >> https://github.com/wasmerio/wasmer/issues/2589 >> >> (and my own posts have started appearing in my Google search queries, so >> it's not like I could keep this a secret even if I wanted to anyway ;-) >> >> Best regards, >> >> Antony >> >> -- >> 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/CAJ48g%2BAUE%3D3qB2PDeDXcqNOg%3DDyT0tBfnTX97XjOKdOV7ukjEw%40mail.gmail.com >> <https://groups.google.com/d/msgid/metamath/CAJ48g%2BAUE%3D3qB2PDeDXcqNOg%3DDyT0tBfnTX97XjOKdOV7ukjEw%40mail.gmail.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/CAFXXJSs4y59VUgNpxSWgXJSKJXv2m5dzLWz%3D9yGtOTtvxZzk0Q%40mail.gmail.com > <https://groups.google.com/d/msgid/metamath/CAFXXJSs4y59VUgNpxSWgXJSKJXv2m5dzLWz%3D9yGtOTtvxZzk0Q%40mail.gmail.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/CAJ48g%2BBO1fSijengHwRGs8UbZU7o3v2UOpdia0E4cpwxH7w9rQ%40mail.gmail.com.
