Hacker News Reader

Comment by s17n | Hacker News Reader

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.

View on HN

> 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.

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.

Indeed, or to summarize as a soundbite: tests can only prove existential properties but types can prove universal properties.

> 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.

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.

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.

And you’re just doubling down on sophistry. Why should anyone take you seriously in this conversation?

Saying "you're doubling down on sophistry" instead of just "you're wrong" doesn't actually make you more convincing.

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.

> There's no such thing as "proving correctness".

Given the caveats you mention, is there such thing as proving anything?

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.

> 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.

> 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.

Reply on news.ycombinator.com