Zulip Chat Archive

Stream: Program verification

Topic: What is the status of program extraction?


view this post on Zulip Agnishom Chattopadhyay (Jun 22 2020 at 00:43):

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?

view this post on Zulip Mario Carneiro (Jun 22 2020 at 00:53):

This is a major component of the Lean 4 architecture

view this post on Zulip Mario Carneiro (Jun 22 2020 at 00:53):

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

view this post on Zulip Mario Carneiro (Jun 22 2020 at 00:55):

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

view this post on Zulip Agnishom Chattopadhyay (Jun 22 2020 at 01:10):

Great, thanks! Rooting for Lean 4


Last updated: May 08 2021 at 21:09 UTC