Cool. I've been working on a compiler for a subset of Lean that targets WASM. The compiler is implemented in Lean. https://github.com/jsmorph/leanexe https:/

Cool. I've been working on a compiler for a subset of Lean that targets WASM. The compiler is implemented in Lean. https://github.com/jsmorph/leanexe https://github.com/jsmorph/leanexe I think I managed to use Talos to prove the WAT generated from an example LeanExe program is correct. ? https://gist.github.com/jsmorph/275a15dc21af037e1d02a1b433bef81f https://gist.github.com/jsmorph/275a15dc21af037e1d02a1b433be... Fun.