[yuppiemephisto]

Lean 4 truly lets you mathematically reason about code and has metaprogramming that truly makes syntax a surface thing, but if anything people who know this have the taste to want better syntax