Lean 4 export Code into another languages

Question

Is it possible to export the Lean language (from Lean 4) into an other language, like Isabelle does is to Haskell or Scala with a code-generation?

Didn't find it in the documentation.

Answer 1

No, and doing so would in general be a bad idea. Lean's run-time performance, especially for primitive types such as Array, fundamentally relies on the "functional but in-place" technique. Languages implemented using tracing garbage collectors usually cannot implement this run-time optimization and so would have to fall back to conservative copying when e.g. modifying arrays.

A better approach is to recognize Lean as a general-purpose language in itself and to use its foreign-function interface (which, yes, is not quite finished and stable as of this writing, but has been used successfully by some people) to interface with code written in other languages.