5 ms·
This is cool because it's in Haskell, but there are a bunch of great formal theorem provers, coq (https://coq.inria.fr/ https://coq.inria.fr/) being one of the
by alokedesai 10y ago
This is cool because it's in Haskell, but there are a bunch of great formal theorem provers, coq (https://coq.inria.fr/ https://coq.inria.fr/) being one of the most famous ones.
- namarkiv 10y agoI 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.