Kakoune
LeanPrism
Paperproof
effectful
metaprogramming
metavariable
monadic
