You might want to look in Lean 4 at some point too. A lot of work has gone into making it's theorem solving ergonomic and approachable for average programmers.
My personal anecdote is that I tried learning Lean 4 last year with a group of other smart and curious programmers, and after a couple of weeks of trying, we failed to make significant progress learning it and stopped. We had much better luck working with Coq instead.
