3 ms·
Haskell isn’t powerful enough to prove your code correct. Agda/Idris/LEAN/… is what you want.
by deterministic 3y ago
Haskell isn’t powerful enough to prove your code correct. Agda/Idris/LEAN/… is what you want.
- corethree 3y agoI'm not talking about proving theorems. I'm talking about creating axioms and creating primitives from axioms. For that any programming language can do it.
- deterministic 3y agoYou are using the word Axiom in a non-standard way. Can you give an example of how you would state an Axiom in Haskell? Here is an example of how it is done in LEAN: axiom propext {a b : Prop} : (a <-> b) → a = b It declares Propositional Extensionality to be true with no evidence/proof.