See also Liquid Haskell https://ucsd-progsys.github.io/liquidhaskell-blog/

Ghost of Departed Proofs https://www.youtube.com/watch?v=2cAxOJEiL00 which talks frankly about these ergonomics