Stream: lean4

Topic: how does "proofs for performance and profit" work?

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 () = true and you know that x and y are 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:

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 implementedBy or 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