The difference between a Hoare Triple/Assertion and a Typed Function

Question

I have been trying to wrap my head around applying Hoare Logic and am running into the question of how Hoare triples are any different from (simply) a typed function.

That is, say you have a typed function $f : A \to B$. The initial state for the function is thus $A$, and the final state is $B$. Similarly, in Hoare Logic, it would be like $\{A\}\ f\ \{B\}$. It's like the Hoare Triple is a typed function application or something, but I'm sure functional programming has those typed as well.

The types could be complex types such as dependent types that have constraints on the input as well, so you can handle things like $x > y$ and the like. So I'm wondering, what the differences are between Hoare Triples and Typed Functions (in any type system) generally.