> No language in the world will save you from having to think about your program's desired behavior, but that doesn't mean we should make it hard on ourselves to even implement the behavior we think we want.
Therein lies the rub. Is there no cost to static typing? Is it not complex? Is it sufficiently expressive? Does it never make it harder to implement the behavior we think we want?
Should everyone write everything in every program in as provable a way as possible? If not, why not?
As the example here shows, there is a cost in effort expended and complexity:
I'm quite glad people are working on these things, and they have genuine benefits. But to overstate the benefits and ignore the costs (as did the post to which I replied) is not productive.
>Does it never make it harder to implement the behavior we think we want?
I should ask why you're aiming at "never"? I prefer to quantify "how often it makes writing harder". It is more useful.
I think that types could make writing behaviour we want even easier. For example, you could use "session types" and be sure that your routers always understand each other. You can write complex algorithm while establishing its complex invariants in types and be sure you're correct.
Therein lies the rub. Is there no cost to static typing? Is it not complex? Is it sufficiently expressive? Does it never make it harder to implement the behavior we think we want?
Should everyone write everything in every program in as provable a way as possible? If not, why not?
As the example here shows, there is a cost in effort expended and complexity:
http://news.ycombinator.com/item?id=2062910
I'm quite glad people are working on these things, and they have genuine benefits. But to overstate the benefits and ignore the costs (as did the post to which I replied) is not productive.