They wrapped Dijkstra and Scholten's predicate transformer semantics [2] in a monad[1]! This almost irrationally pleases me. I'd really love the general concept to get wider traction too. While it's particularly useful for this kind of deep language design, a weakest precondition calculus be used manually when writing code[3] without any particular additional effort once proficiency has been achieved. To use an analogy, it's like the old trick of solving a maze by starting at the end and working backward. Often it ends up being considerably easier.

[1] https://link.springer.com/book/10.1007/978-1-4612-3228-5

[2] https://dl.acm.org/doi/10.1145/2499370.2491978

[3] It pretty much boils down to looking at your code and asking yourself "what has to be true for this to work?" and then writing code that ensures whatever is necessary is true for all possible code paths. Naturally that means limiting possible code paths. There's just one more reason why spaghetti code is bad.