[tom_mellior]

> native code compilation (via C code extraction), allowing you to compile all the constructions you can formalize in Lean directly to native code

Is that really true? What do they do for garbage collection, do they provide their own or use something like the Boehm collector?

As far as I understood, F* also allows C extraction, but only for a subset not including dynamic allocation (or maybe with explicit memory management via effects?).

[cmrx64]

No, it's not true, it "extracts" (compiles) to C++. <https://github.com/leanprover/lean/pull/1241> It's written in Lean itself, as a metaprogram. The code it generates calls into the Lean library ("runtime") for some objects, otherwise uses native types when it can. vm_obj's in Lean are reference counted. There's also in-progress work on an LLVM backend.