Coming from the land of Dijkstra (the Netherlands), I was taught about this in college and it was very cool to use this to prove that post-conditions of a funct

Coming from the land of Dijkstra (the Netherlands), I was taught about this in college and it was very cool to use this to prove that post-conditions of a function are actually true (although finding good loop invariants was sometimes a bit annoying. Denotational semantics are horrible in my opinion, but I really like operational semantics (especially structural operational semantics and natural semantics), they still consider a program as a single mathematical object, but like Hoare logic it also tracks the state before and after each statement. It's really easy to work to with (just apply rules), but sadly it's a bit less powerful than Hoare logic, as you can't infer things that hold in general, you can only reason about specific begin states.