Comment by solomonb

I prefer agda as proof checker but its not a practical choice for building software. Lean feels like it could legitimately become a successor to Haskell as the go to functional programming language for software development.