Lean is actually pretty easy to learn and code in; also, if you are not interested in extreme performance, it is pretty much ready for basic applications (not sure about async and co.).

The problem is that you want to be doing all your coding monadically (so that it looks like the familiar imperative style), and I think there are still many problems about doing proofs on monadic code.