Daniel Fabian (Mar 05 2021 at 10:32):
I'm really excited for lean 4 and I've been following the various lectures. Today I re-visited an older one from about 9 months ago. There's a slide that says you can use proofs to make more efficient machine code.
The examples given were:
- avoiding array bounds checks if you have a proof that your index is in bounds
- avoiding execution of a continuation function
k, if you know that
x = y -> k () = trueand you know that
yare pointer equal
Now, I obviously see how you can write more efficient code by hand if you know these properties hold, but in the slide it said, that the compiler generates better code. How does that work?
Sebastian Ullrich (Mar 05 2021 at 10:54):
The short answer is that the compiler does not know about proofs (only how to detect and eliminate them), but some primitives do:
- https://github.com/leanprover/lean4/blob/e228ca38b812af098046b63f049d3c0e5f6c8e0c/src/Init/Util.lean#L43-L44 (see also https://icfp20.sigplan.org/details/icfp-2020-papers/13/Sealing-Pointer-Based-Optimizations-Behind-Pure-Functions)
In both cases we use optimized but unsafe code (once in C++, once in unsafe Lean) that (we assume) becomes safe by the presence of the proof
Daniel Fabian (Mar 05 2021 at 11:34):
Ah I see, you use the
extern for an efficient manual implementation and use the pure reference implementation for type checking purposes only.
Last updated: May 18 2021 at 23:14 UTC