Natural Number Game in WebAssembly

Stream: lean4

[joaogui1 (he/him)]

So from what I understand NNG3 could run on the client, but NNG4 at the moment needs a server to run. Couldn't we use the fact that lean4 compiles to C to compile that C to WebAssembly and then run it client-side?

[Henrik Böving]

In principle yes, in practice the issue is more of a: someone needs to implement lean -> wasm and nobody as done it yet

[Sebastian Ullrich]

See also https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/web.20editor/near/281494817