The general sentiment of people in the know appears to be:
- Lean 4 is a nice programming language, more ergonomic and easier to learn than Haskell or Idris in many ways. For example, monadic code looks more like Rust than Haskell.
- Given the design choices the language designers made, the implementation could, in time, be made efficient enough to compete with the likes of C and Rust. For example, in-place mutation of collections and data structures is easy to accomplish.
- The tooling and in particular the integration with Visual Studio Code is top-notch.
- The ecosystem and community around Lean 4 as a programming language (as opposed to as a theorem prover) is very small at the moment.
I would add:
- The Lean ecosystem (Mathlib in particular) making use of classical as well as intuitionistic logic has the potential to make theorem proving significantly more palatable than many competing systems.