3 ms·

A correct program is correct whether there's a type system or not. Adding a type system to a correct program doesn't make it more correct. Adding a type syste

by muhuk 12y ago

A correct program is correct whether there's a type system or not. Adding a type system to a correct program doesn't make it more correct. Adding a type system to an incorrect program doesn't make it correct (unless you refactor it). So, type systems DO NOT make programs correct. They help you design correct programs. I am not overlooking the role of static typing in writing correct programs. But I'd disagree if you said type systems by themselves affect correctness of a program directly. A program doesn't come into existence instantly, it is evolved by a design process.

adamnemecek 12y ago
> Adding a type system to an incorrect program doesn't make it correct (unless you refactor it). Of course not, but the compiler will tell you that the program is incorrect since it can deduce it.
- muhuk 12y ago
  This means type systems help you make your program correct, I agree. Your argument was "type systems make your programs correct", I still disagree with that. I think the distinction is important enough.
  - muhuk 12y ago
    Are you downvoting me because you can't stand different opinions?
    - adamnemecek 12y ago
      No, people are downvoting you because you are just wrong. Please see this diagram http://ro-che.info/ccc/17.html http://ro-che.info/ccc/17.html
    - steveklabnik 12y ago
      FWIW, you cannot downvote someone who replies to you. It could not possibly be adamnemecek.
dylukes 12y ago
A type system is a tool. No tool makes anything better without actually using it. Saying that applying a type system to an incorrect program doesn't make it correct without refactoring is like saying hanging a painting with nails doesn't work without a hammer. It's true, but misses the point. Programmers tend to introduce implicit type information (anything from dynamic types to how you choose which functions to apply to which values). Bunches of bits have to be classified somehow to be useful. A static type system lets you specify and define that classification explicitly, rather than implicitly. So, if your mental model of the correctness of a program includes type information (and I assume it does in some manner or another) a static type system is invaluable for proving (re CHC) one facet of the correctness your program. Moreover, if your model isn't perfect – it rarely is – then a type system can allow you to scrutinize and analyze your model more rigorously.
dllthomas 12y ago
A straight line is correct whether it was drawn with a straightedge or not. Adding straightedge to a straight line doesn't make it more straight. Adding a straightedge to an crooked line doesn't make it straight (unless you redraw it). So, straight edges DO NOT make lines straight. They help you draw straight lines. I am not overlooking the role of straightedges in drawing straight lines. But I'd disagree if you said straightedges by themselves affect straightness of a line directly. A blueprint doesn't come into existence instantly, it is evolved by a design process.

by muhuk 12y ago

adamnemecek 12y ago

> Adding a type system to an incorrect program doesn't make it correct (unless you refactor it). Of course not, but the compiler will tell you that the program is incorrect since it can deduce it.

muhuk 12y ago
This means type systems help you make your program correct, I agree. Your argument was "type systems make your programs correct", I still disagree with that. I think the distinction is important enough.
- muhuk 12y ago
  Are you downvoting me because you can't stand different opinions?
  - adamnemecek 12y ago
    No, people are downvoting you because you are just wrong. Please see this diagram http://ro-che.info/ccc/17.html http://ro-che.info/ccc/17.html
  - steveklabnik 12y ago
    FWIW, you cannot downvote someone who replies to you. It could not possibly be adamnemecek.

dylukes 12y ago

A type system is a tool. No tool makes anything better without actually using it. Saying that applying a type system to an incorrect program doesn't make it correct without refactoring is like saying hanging a painting with nails doesn't work without a hammer. It's true, but misses the point. Programmers tend to introduce implicit type information (anything from dynamic types to how you choose which functions to apply to which values). Bunches of bits have to be classified somehow to be useful. A static type system lets you specify and define that classification explicitly, rather than implicitly. So, if your mental model of the correctness of a program includes type information (and I assume it does in some manner or another) a static type system is invaluable for proving (re CHC) one facet of the correctness your program. Moreover, if your model isn't perfect – it rarely is – then a type system can allow you to scrutinize and analyze your model more rigorously.

dllthomas 12y ago

A straight line is correct whether it was drawn with a straightedge or not. Adding straightedge to a straight line doesn't make it more straight. Adding a straightedge to an crooked line doesn't make it straight (unless you redraw it). So, straight edges DO NOT make lines straight. They help you draw straight lines. I am not overlooking the role of straightedges in drawing straight lines. But I'd disagree if you said straightedges by themselves affect straightness of a line directly. A blueprint doesn't come into existence instantly, it is evolved by a design process.