Your intuition is right. Liquid (refinement) types, design by contract and Hoare logic have, essentially, the same expressiveness.

Personally I find refinement types more promising than dependent types, but time will tell.