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

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.