>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.