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