I would like to emphasize that this gives you a theorem prover "inside" haskell, unlike coq/agda where you need to do program extraction. This means you can com

I would like to emphasize that this gives you a theorem prover "inside" haskell, unlike coq/agda where you need to do program extraction. This means you can combine proofs and programs without a significant impact to the runtime performance.