Comment by steego

This is exciting!

Given your experience with Rosetta 2 and your deep understanding of code translation and optimization, what specific areas in Lean’s code generation pipeline do you see as ‘low-hanging fruit’ for improvement?

Additionally, which unique features or capabilities of Lean do you find most promising or exciting to leverage in pushing the boundaries of efficient and high-quality code generation?