If you are interested in this kind of thing, you should check out Dafny. It’s a programming language with Hoare-logic style pre- and postconditions (and the underlying implementation computes weakest preconditions, Dijkstra-style). But what sets it apart is that it is backed by an automatic theorem prover (Z3) which is sufficiently powerful to handle most things that seem trivial to a human. To me Dafny feels like the promise of programming verification research in the 1970s finally came through: you can carry out program verification like you would with pen and paper, without being overwhelmed by finicky algebraic manipulations.
If you are interested in this kind of thing, you should check out Dafny. It’s a programming language with Hoare-logic style pre- and postconditions (and the underlying implementation computes weakest preconditions, Dijkstra-style). But what sets it apart is that it is backed by an automatic theorem prover (Z3) which is sufficiently powerful to handle most things that seem trivial to a human. To me Dafny feels like the promise of programming verification research in the 1970s finally came through: you can carry out program verification like you would with pen and paper, without being overwhelmed by finicky algebraic manipulations.