| > I think you missed the point I was making which is that you still have to know that you're proving the right thing. Right now, it's a missing part in many theorem prover systems (but I didn't do exhaustive researching, so it's more my point of view) : a code to succinctly describe, or state, the problem you are trying to solve. For exemple, for a sorting problem, you would state the problem in English : after sorting, for any element E, the next element in the sequence should be lower. > It's entirely possible to have a but in the proof itself, at which point your program is going to incorrect The premise of theorem provers is that if the problem is correctly stated, then a proof of a solution passing the prover's compiler and a few human reviews is even more unlikely to have a bug. > Reading and understanding the Idris proof is actually more work than understanding the untyped Python version, therefore it's actually harder to say whether it's correct or not in a semantic sense. I would be curious to see a Python proof of the Python sort function. I mean an actual logical and mathematical proof, not a unit test or fuzzy test. It would imply to create a library with a DSL around math and logic. |