• add unsafe keyword.
• allow people to provide unsafe version of any opaque function if the type is inhabited. Type inhabited => proofs are fine. (Do we need to assume UIP for this to work?)
• mimalloc, custom allocator.
• counting immutable beans for optimising refcounting. (related work: Perceus: Grabage free refcounting with reuse.)
• hash tables and arrays are back (thanks to linearity?)
• Tabled typeclass resolution for allowing diamonds in typeclass resolution (typeclasses no longer need to form a semilattice for resolution).
• Discrminiation trees.
• LEAN4 elaborator for adding custom syntax related to monads, tactics.
• Beyond notation: hygenic macro expansion for theorem proving languages.
• Kernel can have external type checker.

during wartime, you do not study the mating ritual of butterflies

• Collaboration: Optimising tensor computations.
• Collaboration: Rust integration.
• Collaboration: DSLs for LEAN.
• Collaboration: SAT/SMT integration

§ Metaprogramming in LEAN4

• macro expansion, elaboration. First expand all macros, elaborate, repeat.

§ Verified decompilation

• We want assured decompilation.
• Check equivalence of BBs using solvers; compcert approach is too complex.

• Lean together 2021