Re:Names are not type safety
by ImprobableTruth on Monday November 02, 2020 @05:36AM
(#24966550)
>In practice, I think reasonably intuitive properties are already very difficult to formalize in refinement types.
Could you elaborate on that? Unless you're just saying that formalizing reasonably intuitive properties is difficult in general, I don't see what you mean.
To add to this:
In theory, it is not just difficult, but impossible.
Imagine that the refinement predicate is whether the String/Text encode a (non-)halting Turing machine/Haskell program. Checking it would solve the halting problem. And this predicate is the proof of Rice theorem.[1] (Granted, this may require some sufficiently powerful logic such as first order, not sure if this proof applies to LiquidHaskell.)
In practice, I think reasonably intuitive properties are already very difficult to formalize in refinement types.