Kakoune
LeanPrism
Paperproof
effectful
monadic
