The idea is that, if you can describe the problem (here, sorting) with a few lines, you don't have to prove that the Idris code is correct, because the machine do it for you. You can throw that sort function without even looking at the code in any critical space mission you want and, if the premises are true, then it will always correctly sort.
You can imagine 3 kinds of code :
- a code that describes the problem (that is both human readable and machine readable)
- a code implementing the solution (here, your Python script)
- a code proving the implementation correctly answers the problem (which would be math if you had to prove your Python code on a whiteboard)
The idea is more about reusing and sharing trusted code, re-running the proof on your own system to make sure it's legit, and move on. You don't need to look at the proof to use the sort function, you would only look at the code that describes the problem and make sure it's the right one for your problem at hand.
>The idea is that, if you can describe the problem (here, sorting) with a few lines, you don't have to prove that the Idris code is correct, because the machine do it for you
The machine can't show that your specification is correct, only that it's self consistent. What you're doing is writing a proof that the compiler will use to verify your code. However, if you make a mistake in your proof, then the compiler will happily verify the wrong thing.
The argument is that it's much harder to spot a mistake in a 300 line Idris proof than it is in a 5 line Python implementation.
> However, if you make a mistake in your proof, then the compiler will happily verify the wrong thing.
I don't use theorem provers in my to day to day tasks, but I had the 101 course at University. Back then I wrote basic proof with the tools, and if your problem is correctly stated and entered in the system, you simply CAN'T arrive to an invalid proof. The only way to fool the compiler is to use logical shortcuts, which are clearly defined in term of language keywords, so you know exactly where is the weakness in the proof, and look for them.
Edit : I don't know every theorem provers out there, so to give a bit more context about my experience, it was with the Coq theorem prover
> if your problem is correctly stated and entered in the system, you simply CAN'T arrive to an invalid proof.
How is that different from: If your problem is correctly stated, and correctly coded into in the system using x86 machine language, then you can't arrive at a bug!
At least in Coq, there is no "bug" when you write a proof, it uses mathematical notations and logical rules to conclude a fact. Because of that you cannot state all the problems you would be able to state with x86. What I meant is that such theorem provers don't give you false-positive : if it tells you your proof is correct, then there can't be a "bug" in your reasoning
In Coq your proof is your program, and if you end up proving the wrong thing that's a bug in the program. There's no magic here. Only a human can tell whether the code does what was intended. To do that you have to understand the code.
If you are proving the wrong statement, then you simply didn't state the initial problem correctly, it has nothing to do with a bug in your proof. It's like saying there is a bug in your implementation of a sort function, while we initially asked you to implement a max function. Even if your sort function is correctly implemented, it's still a "bug" to the person who asked you to implement a max function.
That's my whole point. You're really just pushing the problem as step back instead of solving it. Instead of worrying about bugs in your implementation, you're now worrying about bugs in your specification.
Problem is that these proofs are not the specification. They are very detailed. Specification says "write me a sort function", and the proof is some gobbledygook that deal with irrelevant minutiae of the sorting implementation. Where is the proof which proves that that proof matches the specification?
Because only a human can decide whether the specification matches the intent. This is not a hard concept. The machine can only tell you that your specification is self-consistent, not that it's specifying what you wanted.
The machine could go a level above and helps the human to reflect about its intents. That would basically be a machine convincing the human he/she is already happy right now, and he/she doesn't need to earn more money, and therefore doesn't need that "new e-commerce website". An artificial psychologist conversational agent would help you know about what you really want in life :)
You can imagine 3 kinds of code :
- a code that describes the problem (that is both human readable and machine readable)
- a code implementing the solution (here, your Python script)
- a code proving the implementation correctly answers the problem (which would be math if you had to prove your Python code on a whiteboard)
The idea is more about reusing and sharing trusted code, re-running the proof on your own system to make sure it's legit, and move on. You don't need to look at the proof to use the sort function, you would only look at the code that describes the problem and make sure it's the right one for your problem at hand.