compiler backends

Stream: general

[François Sunatori]

Hi, I'm aware that Agda has compiler backends so that we can compile Agda code into Haskell or Javascript (https://agda.readthedocs.io/en/v2.6.1.3/tools/compilers.html?highlight=backend#backends). I was wondering if this exists in Lean as well. If it isn't, are there any plans to support such a feature? Thanks!

[Bryan Gin-ge Chen]

There's nothing like that for Lean 3 (although you can run a WebAssembly version of the Lean 3 interpreter in the browser - see e.g. #webeditor).

Lean 4 can be compiled to C, though I don't think the details have been added to the docs yet.

[François Sunatori]

Thanks @Bryan Gin-ge Chen! I'm not sure the WebAssembly interpreter option is what I would like though.. Do you know if anyone has ever used Lean in order to compile proven code into another language (a bit like Extraction in Coq)? I'm a web developer and would love the ability to write proofs in Lean that compile to Javascript (to run code that has been proven rather than depending only on unit tests). I guess with Lean 4 at least it will be doable in C?

[Bryan Gin-ge Chen]

I don't know if anyone has done so yet, but I think a lot of folks are aiming to do that eventually. See e.g. this post.

(I'm probably not the right person to ask about this.)