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.