The power-to-weight ratio of refinement types is as unclear as that of contracts. You get more expressivity than simple types, but it's unclear whether it's eno

The power-to-weight ratio of refinement types is as unclear as that of contracts. You get more expressivity than simple types, but it's unclear whether it's enough to make a real impact. On the other hand, we're nowhere near being able to verify the properties that would make a real impact on code sizes that truly matter with automated proof techniques. Types are a bad fit for "deep" properties to begin with because they're tied to the proof theory of the type system. At least contracts have some leeway, as they can be verified more weakly but with much more scalable techniques (like randomized tests).