Comment by nextos

If verification is the goal, but you don't want to learn theorem proving yet, Dafny is really approachable and practical [1]. F* is also worth considering as a proof-oriented alternative to Isabelle that is focused on software verification [2]. Why3, Rocq and Agda are other obvious contenders.

[1] https://dafny.org/latest/OnlineTutorial/guide

[2] https://fstar-lang.org/tutorial