"So, for me, that’s as far as increasing our ability to give you statically guaranteed theorems about Haskell programs.
My money’s on Liquid Haskell at the moment and I hope that we the Haskell community"
My experience is that other refinement type systems are way less complex. See: https://github.com/hwayne/lets-prove-leftpad
In particular, compare https://github.com/hwayne/lets-prove-leftpad/blob/master/liq... to https://github.com/hwayne/lets-prove-leftpad/blob/master/daf...
For me this has been a bit of a disappointment.