What is the status of program extraction?

Stream: Program verification

[Agnishom Chattopadhyay]

From a quick google search, I hear that there is some plan of supporting extracting Lean to C++ some day. What is the current status of this?

[Mario Carneiro]

This is a major component of the Lean 4 architecture

[Mario Carneiro]

It's not likely to happen in lean 3 as it seems lean 4 is imminent

[Mario Carneiro]

In lean 3, we have the VM instead, which is an interpreter for lean programs. I think lean 4 will also have an interpreter, but at the end of a file it transpiles to C and then compiles using clang (?) to produce machine code that can be run in the next file

[Agnishom Chattopadhyay]

Great, thanks! Rooting for Lean 4

[Kevin Cheung]

Reviving this old thread. What's the current status of program extraction in Lean 4?

[Henrik Böving]

Lean 4 is a self hosted programming language that can compile to both C and LLVM.

[Karl Palmskog]

traditionally, extraction implies preservation of meaning (in some sense). What semantics of C and LLVM does Lean (currently) use?

[Henrik Böving]

There are no formal semantics, its just a normal compiler like you would see in other programming languages.

[Kevin Cheung]

What would be the workflow if one wants to write formally verified code? Write the code in Lean in one file, prove correctness in Lean in a separate file, then compile the former into LLVM?

[Henrik Böving]

You can just put them into the same file it doesn't matter. But yes that works.

[Joe Hendrix]

Pragmatically, just getting started is as simple as running lake init, lake build and then your executable will be in .lake/build/bin.

Lean does have very little support for verification of code in the IO monad though, so the verified parts will almost certainly need to be pure at least for the time being.

[Bulhwi Cha]

Kevin Cheung said:

What would be the workflow if one wants to write formally verified code? Write the code in Lean in one file, prove correctness in Lean in a separate file, then compile the former into LLVM?

Do I need to write a formal semantics of Lean in itself to prove the correctness of my Lean code in Lean? I don't know much about formal verification, so forgive me if my question is unclear.

[Henrik Böving]

It highly depends on what kind of verification you are after and what trusted code base you are willing to accept. If you do proves about the behavior of Lean code in Lean you have effectively shown that the view which the kernel has on your code does have property X while only trusting the Kernel.

However the view which the kernel has on your code is not the view which gets executed, Lean's compiler splits apart from the elaborator quite a bit before we ever end up reaching the kernel. So now you have basically two choices:

1. Just trust the Lean compiler and the transitions it makes, this is pretty much what everyone does and it is perfectly reasonable. It is also the trust model that basically every other language in this world has.
2. Think about precise semantics for the various IRs used by the compiler and formally verify all compiler passes. Note that core currently has no interest in doing this at all so if we end up changing a part of the compiler it would be the job of whoever wishes to verify it to fix their proofs. In general I'm rather confident that a verification of the compiler is close to impossible without the authors of the compiler specifically designing it such that it is possible. This is simply because we have partial functions around already so someone who verifies stuff already can't look into those and would have to change compiler code.

[Bulhwi Cha]

Thanks for your detailed explanation.

[Andrés Goens]

Just for completeness (although I think that @Henrik Böving is right that 1. is perfectly reasonable), there is a third option: write your own (less optimized) verified or a verifying (in the sense of translation validation) compiler. Probably a lot of effort for little gain, but still probably more feasible than keeping up with core on the regular compiler

[Siddharth Bhat]

For the record:

write your own (less optimized) verified or a verifying (in the sense of translation validation) compiler

is (vaguely) what I aim to do in my PhD, but it's pretty unclear how far we will get.