## § LEAN 4 overfrom from LEAN together 2021

- 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.