Lean Compilation to Other Languages

Stream: new members

[Daniel Geisz]

Hey all, I've been looking a bit at Dafny and noticed that it compiles to a bunch of different languages (Go, Python, Java, etc). Wondering if there's anything similar in Lean or any desire for something like this? Just would be cool if you could write a verified program in Lean and then compile it to another more common language for use there

[Bulhwi Cha]

Honestly, I'm satisfied with using Dafny to write a verified program and compile it into other languages.

[Johan Commelin]

Atm the only options are C and WebASM I think

[Eric Wieser]

Writing CPython / lean bindings would be a nice project

[Eric Wieser]

(that is, code to convert between basic lean_object* types and PyObject*s)

[Eric Wieser]

Then you could compile lean to C code, then write / generate a small wrapper to create python bindings for that C code

[Sebastian Ullrich]

The general answer here is that Lean does not compile to other languages as it is a general-purpose language in itself. So you do like you do in other general-purpose languages and use FFI to communicate with external languages.

[David⚛️]

Eric Wieser said:

Then you could compile lean to C code, then write / generate a small wrapper to create python bindings for that C code

I've been trying to compile lean to C code but is not working for me

[Eric Wieser]

What have you tried? This is supported natively by lake

[Tom]

Eric Wieser said:

Writing CPython / lean bindings would be a nice project

I am about to embark on reading more about Lean's FFI, even though my understanding is that it's still... provisional/unstable?

I've done a lot of work with Python/C++ bindings. What are you imagining you would use the bindings for? Are you looking to call compiled Lean code from Python, or calling Python functionality (e.g. numpy?) from Lean?