VOD: https://www.youtube.com/watch?v=9EN1jA2Q57c

Verification of Program Optimisations (Lean)

Agenda. After the previous stream I realised that optimisations should work as functions over an AST (not a Lean Expr!). Doing optimisations functions over an AST allows you to prove things a lot easier, but requires a lot more work in the form of denotational semantics.

I promised myself I would never go anywhere near those things, but it absolutely makes sense if you want to transpile these verified optimisations to other programs (for example, export optimisations to C for someone’s optimiser).

• Typical example: not every optimisation is going to be a braindead rewrite, the most important optimisation to get down is actually canonicalisation up to AC (associativity, commutativity), that is, LLVM reassociate.

• Introduce denotational semantics. ✅ 2025-12-26
• Implement denotational semantics, and a tactic that actually performs the rewriting and optimisation (with proof).

Aftermath

• Continue furthering the implementation of reify.