I used Why3 for a while, but eventually found that Dafny had a better user experience.
Currently I work on Dafny verifications. It was so tough that when I wrote Dafny code I felt as confused as when I took the first programming class when I entered the college.
But it was a lot of fun, for sure. I think the proofs written this way are quite self-explanatory. I think the proofs are quite readable for humans (at least compared to Coq's so exotic-looking tactic language), so I believe that learning algorithms (along with their proofs) through Dafny code is a nice experience too.
My other repo specialized in verifying LeetCode problems using Dafny