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