Can we just develop in Lean and compile to something else for speed?

Lean is actually pretty speedy as is, and it enables much harder optimizations[1]

[1] https://github.com/kim-em/lean-zip#verification-enables-perf...

Of course.