The difference between a Hoare Triple/Assertion and a Typed Function
You are putting your finger on angular stone of program verification.
At a very rough and high level you can think a derivation in Hoare logic as proving a property, thing which can somehow be translated in a type derivation. 

More precisely you are almost (you're slightly limiting yourself with Hoare logic) rediscovering the very deep Curry-Howard correspondence with asserts that mathematical proof and type derivation are the same thing.