[kmill]

Yes to all. In Lean 3, they found it was great being able to write tactics in Lean itself, which has led to many nice tactics in mathlib. Lean 4 consolidates many lessons learned, and most of Lean itself is written in Lean now. In principle they'll be able to prove different parts of the Lean system are correct (eventually).

Lean has a C backend, so you can write in Lean, prove your program meets the spec, then output reasonably optimized (but impenetrable) C code.

I made this raytracer partly to see how efficient that code would be (I haven't gotten around to comparing it to anything yet, though), partly to try writing a real program in Lean rather than my usual theorem proving, and partly to better understand ray tracers.

In principle, one could prove this raytracer (once fully debugged :-) ) converges to the theoretical solution to the rendering equation, with arbitrary precision floats. This would be an ungodly amount of work to carry out right now in Lean 4, but it's in principle doable, I think.

[mbrodersen]

It would be really interesting to know how fast the LEAN 4 version is compared with C/C++.

[kmill]

I ended up writing one in the meantime -- check out the end of the readme. For this workload it seems to be a factor of 30x. The C program gets away with no heap allocation and inlining the entire render loop, though Lean does do quite a lot of unboxed float arithmetic. I tried to optimize the Lean and only shaved 25% off the runtime (code in a branch).

I suspect that it could be made a bit faster if each thread had its own copy of the scene. Lean handles reference counting of shared objects differently.