Chris Done (2022-05-26T18:09:31.030304903+00:00) Permalink

Valid concerns!

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