3 ms·

reminds me a little of eiffel's design by contract. it looks really promising

• nextos 3y ago
  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.
• tgv 3y ago
  It made me wonder too, what the (practical) advantage over contracts is. If anything, Liquid Types seem less powerful. E.g., you can't use it to express a relation between two function parameters. It seems to be a macro for contracts (the type name implicitly copies its restriction as a contract clause), so in that sense it could be welcome as a practical way of improving correctness.