[kmill]

I use Lean 4 quite a lot these days, and I appreciate how the developers embrace syntax extension and metaprogramming solutions rather than trying to encode complicated control flow using ascii art operators (it's like Lisp meets the ML family). I suppose programming with dependent types is enough of a challenge, so why make it even harder? They've got a sophisticated "do" notation with imperative constructs, mutable variables (that are translated into something StateT-like), and pretty seamless monad lifting. They've also got pipeline operators, including things like `x |>.foo a b c` for `X.foo x a b c` if `x` has type `X` (type-directed field notation is wonderful).

Many times you don't even use currying, since it's not always worth the effort making a particular argument be the last one. Instead you might write `xs.map (f · x)`, where `(f · x)` is short for `fun a => f a x`.

The language also has an interesting GC that lets you write functional algorithms that have good memory performance -- objects with exactly one reference can be mutated (using so-called FBIP, "functional but in-place"). There's an Array type whose theoretical representation is a linked list but whose run-time representation is a dense array with O(1) pushing, popping, and writing. Makes it easy to write performant code without resorting to sophisticated functional data structures.