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.