Hacker News Reader

Comment by muhuk | Hacker News Reader

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.

View on HN

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.

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.

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

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.

Are you downvoting me because you can't stand different opinions?

No, people are downvoting you because you are just wrong.

Please see this diagram

http://ro-che.info/ccc/17.html

FWIW, you cannot downvote someone who replies to you. It could not possibly be adamnemecek.

Reply on news.ycombinator.com