3 ms·

> If you're going to take the trouble to specify that it's an integer list, might as well use a statically typed language, right? When you use a dynamically typ

> If you're going to take the trouble to specify that it's an integer list, might as well use a statically typed language, right? When you use a dynamically typed language, presumably the point is to not have to worry about static types. Yes, I said that. :) > > "Soundness" is a mathematically defined concept, but a very binary one (it's sound or it isn't). > That's precisely why it's better! Well... it's better for some purposes, but it doesn't allow us to talk about most languages effectively. None of the top 10 most commonly-used languages in industry today are soundly typed. If memory serves me, in fact, the only language I know of with a mature implementation that's soundly typed is ML. So it's a useful concept in a very specific context, but not that useful for talking about most languages. > I'm not so sure about this one. Although Java is certainly safer than C, because it replaces undefined behavior with a battery of runtime checks (just like a dynamic language), I feel it's about equally difficult in Java and C to translate my thoughts into types. Basically I think what you're describing about Java is a mixture of mid-strength static typing and relatively strong dynamic typing. At least, that's how I'd describe it. C does no real checking i.e. around `void` pointers, adding integers to pointers, tagging unions, etc., at compile time or at runtime, which is why I claim it's a very weakly-typed language (and also why I tend to avoid some of those features).

catnaroek 10y ago
> Basically I think what you're describing about Java is a mixture of mid-strength static typing and relatively strong dynamic typing. At least, that's how I'd describe it. For me, the real payoff of using a static type system is enforcing the invariants I care about. In other words, a type system is a tool that partially relieves me of my proof obligation as a programmer. A “type system” that doesn't do this is just annoying ceremony. So, if we insist on calling type systems “strong” and “weak”, this is still a binary question: a type system is either capable (“strong”) or incapable (“weak”) of expressing what I want to express in a crisp, elegant, crystal clear way. From this point of view, Java is just as unacceptable as C, perhaps even more so, because C at least has the decency not to pretend it has much of a type system. OTOH, it seems that, to you, and perhaps most programmers, a type system is merely a tool for preventing catastrophic errors. If that's your only goal, then turning catastrophic errors (say, memory corruption) into less catastrophic ones (say, raising exceptions everywhere) is a perfectly valid approach, and of course Java is “more strongly typed” than C. This can be useful or harmful, depending on what kind of program you're writing, but I refuse to call it a type system.

catnaroek 10y ago

> Basically I think what you're describing about Java is a mixture of mid-strength static typing and relatively strong dynamic typing. At least, that's how I'd describe it. For me, the real payoff of using a static type system is enforcing the invariants I care about. In other words, a type system is a tool that partially relieves me of my proof obligation as a programmer. A “type system” that doesn't do this is just annoying ceremony. So, if we insist on calling type systems “strong” and “weak”, this is still a binary question: a type system is either capable (“strong”) or incapable (“weak”) of expressing what I want to express in a crisp, elegant, crystal clear way. From this point of view, Java is just as unacceptable as C, perhaps even more so, because C at least has the decency not to pretend it has much of a type system. OTOH, it seems that, to you, and perhaps most programmers, a type system is merely a tool for preventing catastrophic errors. If that's your only goal, then turning catastrophic errors (say, memory corruption) into less catastrophic ones (say, raising exceptions everywhere) is a perfectly valid approach, and of course Java is “more strongly typed” than C. This can be useful or harmful, depending on what kind of program you're writing, but I refuse to call it a type system.