7 ms·

I hope you realize the Idris code actually prove that the list will be correctly sorted, unlike your python code.

by olzd 8y ago

kazinator 8y ago
I am skeptical; prove that it proves such a thing. Might it not actually be easier to prove that the Python code sorts than that the Idris code proves sorting?
- antpls 8y ago
  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.
  - yogthos 8y ago
    >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.
    - antpls 8y ago
      > 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
      - kazinator 8y ago
        > 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!
        antpls 8y ago
        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
        yogthos 8y ago
        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.
        antpls 8y ago
yogthos 8y ago
I think you missed the point I was making which is that you still have to know that you're proving the right thing. It's entirely possible to have a but in the proof itself, at which point your program is going to incorrect. 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.
- pka 8y ago
  “Saying it’s correct in the semantic sense” = proving the code. They found a bug in Java’s binary search after 10 years of it going unnoticed, so I think you’re overestimating your own ability to prove code correct in your head. Generative testing/spec is absolutely useful. It doesn’t subsume static typing and much less theorem proving though, and you can QuickCheck your pre and postconditions in static languages as well.
  - yogthos 8y ago
    I don't find that to be a convincing argument in the slightest. The type system in Java also failed to catch the bug, and there's no guarantee that you wouldn't end up with an error in a specification using a more advanced type system that could actually encode that constraint. The thing to realize is that theorem proving is not a business goal in most cases. What you care about is being able to deliver software that works well in a reasonable amount of time. Sure, you might end up with a binary search bug in your code that goes unnoticed for 10 years, but clearly the world didn't stop because of that, and people have successfully delivered many projects in Java despite that bug that work perfectly fine.
    - pka 8y ago
      > The type system in Java also failed to catch the bug Java is not a theorem prover, and your comment was about theorem provers. > you wouldn't end up with an error in a specification Again, completely orthogonal to your argument. If you have an error in specification tests won't help you because you'll test the wrong thing. > The thing to realize is that theorem proving is not a business goal in most cases. What you care about is being able to deliver software that works Again, your comment was about "saying things are correct in the semantic sense". You're saying now "I don't care about correctness in the semantic sense, I care about delivering software that "works" (whatever this means; clearly it doesn't mean software without bugs) in a reasonable amount of time" and that's fine. I do too, but again, nothing to do with your original argument.

I hope you realize the Idris code actually prove that the list will be correctly sorted, unlike your python code.

by olzd 8y ago

I hope you realize the Idris code actually prove that the list will be correctly sorted, unlike your python code.

I am skeptical; prove that it proves such a thing. Might it not actually be easier to prove that the Python code sorts than that the Idris code proves sorting?

antpls 8y ago
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.
- yogthos 8y ago
  >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.
  - antpls 8y ago
    > 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
    - kazinator 8y ago
      > 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!
      - antpls 8y ago
        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
        yogthos 8y ago
        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.
        antpls 8y ago

yogthos 8y ago

I think you missed the point I was making which is that you still have to know that you're proving the right thing. It's entirely possible to have a but in the proof itself, at which point your program is going to incorrect. 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.

pka 8y ago
“Saying it’s correct in the semantic sense” = proving the code. They found a bug in Java’s binary search after 10 years of it going unnoticed, so I think you’re overestimating your own ability to prove code correct in your head. Generative testing/spec is absolutely useful. It doesn’t subsume static typing and much less theorem proving though, and you can QuickCheck your pre and postconditions in static languages as well.
- yogthos 8y ago
  I don't find that to be a convincing argument in the slightest. The type system in Java also failed to catch the bug, and there's no guarantee that you wouldn't end up with an error in a specification using a more advanced type system that could actually encode that constraint. The thing to realize is that theorem proving is not a business goal in most cases. What you care about is being able to deliver software that works well in a reasonable amount of time. Sure, you might end up with a binary search bug in your code that goes unnoticed for 10 years, but clearly the world didn't stop because of that, and people have successfully delivered many projects in Java despite that bug that work perfectly fine.
  - pka 8y ago
    > The type system in Java also failed to catch the bug Java is not a theorem prover, and your comment was about theorem provers. > you wouldn't end up with an error in a specification Again, completely orthogonal to your argument. If you have an error in specification tests won't help you because you'll test the wrong thing. > The thing to realize is that theorem proving is not a business goal in most cases. What you care about is being able to deliver software that works Again, your comment was about "saying things are correct in the semantic sense". You're saying now "I don't care about correctness in the semantic sense, I care about delivering software that "works" (whatever this means; clearly it doesn't mean software without bugs) in a reasonable amount of time" and that's fine. I do too, but again, nothing to do with your original argument.