How is this different from preventing stupid people from doing stupid things?
I've said this recently, but I like static typing when it contributes to the essential details of the program, rather than merely being a redundant layer for enhancing confidence in one's own code. Static typing is particularly meaningful at module boundaries, where it lets people establish confidence about each other's programs.
Anyway, enhanced usability is nothing to scoff at either. If you find this kind of static analysis important, I look forward to what you accomplish. :)
"How is this different from preventing stupid people from doing stupid things?"
Because the only difference is whether the error occurs at compile-time or run-time. I'm not adding in additional restrictions to make the type-system happy: if the type system can't understand it, it just defers the checking until run-time.
Thus, the type system takes certain errors that would have happened at run-time, and instead makes them happen at compile-time, which is better because it gives you early error detection. What the type system doesn't do is restrict the programmer in order to make it easier to detect errors at compile-time.
---
"If you find this kind of static analysis important"
Not really, no. Useful? Yeah, a bit. It's nice to have some early detection on errors. But my goals aren't to guarantee things. So whether you have the type-checker on or off just determines when you get the errors. A small bonus, but nothing huge. So I'd be fine with not having any static type checker at all.
The way I see it, what you're talking about still seems like a way to cater to stupid programming. Truly smart programmers don't generate any errors unless they mean to. ;)
---
"What the type system doesn't do is restrict the programmer in order to make it easier to detect errors at compile-time."
Guarantees don't have to "restrict the programmer." If you take your proposal, but add a type annotation form "(the <type> <term>)" that guarantees it'll reject any program for which the type can't be sufficiently proved at compile time, you've still done nothing but give the programmer more flexibility. (Gradual typing is a good approach to formalizing this sufficiency: http://ecee.colorado.edu/~siek/gradualtyping.html)
I think restriction comes into play when one programmer decides they'll be better off if they encourage other programmers to follow certain conventions, or if they follow certain conventions on their own without immediate selfish benefit. This happens all the time, and some may call it cargo culting, but I think ultimately it's just called society. :-p
"The way I see it, what you're talking about still seems like a way to cater to stupid programming. Truly smart programmers don't generate any errors unless they mean to. ;)"
Then I'll reclarify and say "any programmer who's just as smart as me", thereby nullifying the argument that a "sufficiently smart programmer would never make the mistake in the first place".
---
"If you take your proposal, but add a type annotation form [...]"
Sure, if it's optional. And not idiomatic to use it all the time. The problem that I see with languages that emphasize static typing is that even if it's technically possible to disable the type checker, it's seen as very bad form, and you'll get lots of bad looks from others.
The idioms and what is seen as "socially acceptable" matter just as much as whether it's "technically possible". If I add in type checking, it'll be in a care-free "sure use it if you want, but you don't have to" kind of way. I've seen very few languages that add in static typing with that kind of flavor to it.
---
"This happens all the time, and some may call it cargo culting, but I think ultimately it's just called society. :-p"
And I am very much so against our current society and its ways of doing things, but now we're straying into non-programming areas...
"And I am very much so against our current society and its ways of doing things, but now we're straying into non-programming areas..."
Yeah, I know, your and my brands of cynicism are very different. :) Unfortunately, I actually consider this one of the most interesting programming topics right now. On the 20th (two days ago) I started thinking of formulating a general-purpose language where the primitives are the claims and communication avenues people share with each other, and the UI tries its best to enable a human to access their space of feedback and freedom in an intuitive way.
I'd like to encourage others to think about how they'd design such a system, but I know this can be a very touchy subject. It's really more philosophy and sociology than programming, and I can claim no expertise. If anyone wants to discuss this, please contact me in private if there's a chance you'll incite hard feelings.
