How to do proofs: practically proving properties about effectful programs' results (functional pearl)
Koen Jacobs, Andreas Nuyts, Dominique Devriese · 2019
Dependently-typed languages are great for stating and proving properties of pure functions. We can reason about them modularly (state and prove their properties independently of other functions) and non-intrusively (without modifying their implementation). But what if we are interested in properties about the results of effectful computations? Ideally, we could keep on stating and proving them just as nicely.