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.
