Program in Lean and compile direct in WASM

Stream: general

[Petrica Chiriac]

Is it possible to program in Lean language or in an subset of lean language and to compile that program in WASM?
I am looking for language in which I can demonstrate properties or demonstrate correctness (like Lean) and to directly compile to WASM for running.

I don't want to compile full lean system, only small program that I write.

[Anne Baanen]

Lean 4 is compiled by first translating to C, and you should be able to take that C code and compile to WASM just like ordinary C code. I don't know any details about either of those two steps though...

[Sebastian Ullrich]

You will need Emscripten to use Lean 4's runtime. Or write your own.