Is it really better than Lean though? I started learning programming in Haskell but gradually transitioned into Lean, both because it has almost everything Haskell has (minus laziness), great meta-programming support, and most importantly allows me to drop down into proofs / formal verification if needed.