You might like looking at Dafny. It is more imperative focus, but has many of the same software proving functionality that Lean has.

It is different in that it uses SMT instead of dependent types and tactics to prove the software, but I found it more approachable.

Also, it compiles to several target languages, whereas Lean 4 only compiles to C and therefore only supports the C ABI.