5 ms·

There's no such thing as "proving correctness". You can have bugs in the type definitions. You can have bugs in the english (or whatever your native language

by s17n 9y ago

There's no such thing as "proving correctness". You can have bugs in the type definitions. You can have bugs in the english (or whatever your native language is) description of what you think the algorithm should be doing. You can prove a program does what the types say it should do but that is not what "correctness" means. >Now a big part of the problem is expressing with sufficient accuracy what the properties of the algorithm you want to prove are. For example for string reverse I may want to show more than that `reverse (reverse s) = s`. Since after all if reverse does nothing that would still be true. I would probably want to express that the first and last chars swap when I just call reverse xs. This is no different from writing tests in a dynamic language.

seanwilson 9y ago
> There's no such thing as "proving correctness". You can have bugs in the type definitions. You can have bugs in type definitions and you can have bugs in tests as well and that'll be a problem until computers can read our minds. Type definitions are superior at checking what you specified though because the checking is exhaustive. Perfect is the enemy of good and all that. > This is no different from writing tests in a dynamic language. It's not. In that example, the type system will verify the stated property is true for all values of "s". Tests only check some specific examples whereas using types in this way tests all possible input and output pairs. It's like comparing a maths proof to checking an equation holds for a few examples you tried.
deleted 9y ago
[deleted]
solidsnack9000 9y ago
> There's no such thing as "proving correctness". Given the caveats you mention, is there such thing as proving anything?
- s17n 9y ago
  There are two meanings of prove. The one that type theorists are using is roughly "to derive your statement from axioms with pure logic." This sense of the term can never apply to things in the real world, like programs (of course, a program also exists both as an abstraction about which things can be proved, but when you're talking about programs which are actually doing things in the real world, you can't treat them as being pure logic). The second sense is the scientific "gather enough supporting evidence that your are reasonably sure". In this sense, you can prove a lot of things.
  - solidsnack9000 9y ago
    > There are two meanings of prove. The one that type theorists are using is roughly "to derive your statement from axioms with pure logic." This sense of the term can never apply to things in the real world... I am not sure it's a meaningful distinction. There are no triangles in the "real" world -- if you look close under a microscope, there will be more than three sides -- but geometry proves to be of great practical value just the same.
naasking 9y ago
> This is no different from writing tests in a dynamic language. Types and tests are not equivalent. This is a prevalent myth among dynamic typing enthusiasts. There is no unit test that can ensure, eg. race and deadlock freedom, but there are type systems that can do so. There are many such properties, and tests can't help you there. Types verify stronger properties than tests will ever be able to, full stop. You don't always need the stronger properties of types, except when you do.
- zbobet2012 9y ago
  To add some color here on the difference between a type proof and a test: consider that you can never test all possible strings for reverse. However, a type proof can show that reverse, reverses all possible strings. It is possible to test that a function on 16 bit integers returns the correct value for all inputs. Doing so would be a proof by exhaustion. Type based proofs let us prove things using other methods than exhaustion, which is the only possible way to prove things with tests. That is an important property.
  - naasking 9y ago
    Indeed, or to summarize as a soundbite: tests can only prove existential properties but types can prove universal properties.
catnaroek 9y ago
> You can have bugs in the english (or whatever your native language is) description of what you think the algorithm should be doing. According to the principle of separation of concerns, this isn't the programmer's problem. > You can prove a program does what the types say it should do but that is not what "correctness" means. Of course, the ultimate arbiter of what “correctness” means is the program specification.
eastWestMath 9y ago
No, I’m pretty sure there’s a pretty large body of academic and industrial research on proving program correctness that you can’t just hand wave away with sophistic “but what if your type signature is wrong” nonsense. And there’s a huge difference between a test and a proof - a test can only tell you a program doesn’t do what you think it should for a particular case, a proof tells you that your program does exactly what it is supposed to.
- s17n 9y ago
  Defining "correctness" in terms of types is the CS equivalent of defining "risk" in terms of volatility - it replaces a real and fundamentally unsolvable problem with a problem that, while it has the advantage of being tractable, isn't actually all that important to solve. Great for publishing papers, dangerous when people start confusing the fake problem and the real problem.
  - eastWestMath 9y ago
    And you’re just doubling down on sophistry. Why should anyone take you seriously in this conversation?
    - s17n 9y ago
      Saying "you're doubling down on sophistry" instead of just "you're wrong" doesn't actually make you more convincing.
      - eastWestMath 9y ago
        No, I’m saying sophistry contributes nothing to the conversation. I don’t care about convincing you about the subject at hand: you have the opinion of someone who’s invested too much into justifying their ignorance to actually pick up a textbook and learn the relevant material.

by s17n 9y ago

seanwilson 9y ago

> There's no such thing as "proving correctness". You can have bugs in the type definitions. You can have bugs in type definitions and you can have bugs in tests as well and that'll be a problem until computers can read our minds. Type definitions are superior at checking what you specified though because the checking is exhaustive. Perfect is the enemy of good and all that. > This is no different from writing tests in a dynamic language. It's not. In that example, the type system will verify the stated property is true for all values of "s". Tests only check some specific examples whereas using types in this way tests all possible input and output pairs. It's like comparing a maths proof to checking an equation holds for a few examples you tried.

deleted 9y ago

[deleted]

solidsnack9000 9y ago

> There's no such thing as "proving correctness". Given the caveats you mention, is there such thing as proving anything?

s17n 9y ago
There are two meanings of prove. The one that type theorists are using is roughly "to derive your statement from axioms with pure logic." This sense of the term can never apply to things in the real world, like programs (of course, a program also exists both as an abstraction about which things can be proved, but when you're talking about programs which are actually doing things in the real world, you can't treat them as being pure logic). The second sense is the scientific "gather enough supporting evidence that your are reasonably sure". In this sense, you can prove a lot of things.
- solidsnack9000 9y ago
  > There are two meanings of prove. The one that type theorists are using is roughly "to derive your statement from axioms with pure logic." This sense of the term can never apply to things in the real world... I am not sure it's a meaningful distinction. There are no triangles in the "real" world -- if you look close under a microscope, there will be more than three sides -- but geometry proves to be of great practical value just the same.

naasking 9y ago

> This is no different from writing tests in a dynamic language. Types and tests are not equivalent. This is a prevalent myth among dynamic typing enthusiasts. There is no unit test that can ensure, eg. race and deadlock freedom, but there are type systems that can do so. There are many such properties, and tests can't help you there. Types verify stronger properties than tests will ever be able to, full stop. You don't always need the stronger properties of types, except when you do.

zbobet2012 9y ago
To add some color here on the difference between a type proof and a test: consider that you can never test all possible strings for reverse. However, a type proof can show that reverse, reverses all possible strings. It is possible to test that a function on 16 bit integers returns the correct value for all inputs. Doing so would be a proof by exhaustion. Type based proofs let us prove things using other methods than exhaustion, which is the only possible way to prove things with tests. That is an important property.
- naasking 9y ago
  Indeed, or to summarize as a soundbite: tests can only prove existential properties but types can prove universal properties.

catnaroek 9y ago

> You can have bugs in the english (or whatever your native language is) description of what you think the algorithm should be doing. According to the principle of separation of concerns, this isn't the programmer's problem. > You can prove a program does what the types say it should do but that is not what "correctness" means. Of course, the ultimate arbiter of what “correctness” means is the program specification.

eastWestMath 9y ago

No, I’m pretty sure there’s a pretty large body of academic and industrial research on proving program correctness that you can’t just hand wave away with sophistic “but what if your type signature is wrong” nonsense. And there’s a huge difference between a test and a proof - a test can only tell you a program doesn’t do what you think it should for a particular case, a proof tells you that your program does exactly what it is supposed to.

s17n 9y ago
Defining "correctness" in terms of types is the CS equivalent of defining "risk" in terms of volatility - it replaces a real and fundamentally unsolvable problem with a problem that, while it has the advantage of being tractable, isn't actually all that important to solve. Great for publishing papers, dangerous when people start confusing the fake problem and the real problem.
- eastWestMath 9y ago
  And you’re just doubling down on sophistry. Why should anyone take you seriously in this conversation?
  - s17n 9y ago
    Saying "you're doubling down on sophistry" instead of just "you're wrong" doesn't actually make you more convincing.
    - eastWestMath 9y ago
      No, I’m saying sophistry contributes nothing to the conversation. I don’t care about convincing you about the subject at hand: you have the opinion of someone who’s invested too much into justifying their ignorance to actually pick up a textbook and learn the relevant material.