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
No comments yet.