The secret of Lean4 is that its actually a great programming language, sort like a super Haskell. In fact I like it more as a programming language then as a proof checker!
Dependent types are awesome for regular programming in addition to formal verification. For proof checking I actually prefer Agda.
I wanted to know if Lean 4 is usable for an everyday web app yet, not just for proofs, so I built RealWorld (the Medium clone) in it, frontend included, using Datastar. Looks like it's feasible now with the new libraries. This post describes the experience
Dependent types are awesome for regular programming in addition to formal verification. For proof checking I actually prefer Agda.