Wow, this is fantastic. Now I have a word ("safyness") for what I and others have been saying for so long: that static typing prevents the bugs that are easiest to catch. If it were free, I would take it, but it often does so at a large cost to productivity, and even understanding of the dynamic/runtime behavior of the system.
That second problem I summarize using the phrase the "map is not the territory". (http://en.wikipedia.org/wiki/Map%E2%80%93territory_relation) I had heard this phrase for many years, outside the context of programming. I never quite understood what it meant until I spent time around hardcore C++ and Haskell people. Static typing is a model (a map) for runtime behavior.
what I and others have been saying for so long: that static typing prevents the bugs that are easiest to catch
Not only are such bugs the easiest to catch, but they include bugs that can be insidious, expensive, and prohibit certain refactorings if they are not caught.
This isn't to say that static typing is the only way. It's more accurate to say: If you aren't catching those bugs automatically, you are doing it wrong.
Right. And it's not just that the typing is static, but that you are using it properly. Cf:
struct price { int value; };
struct quantity { int value; };
int placeOrderUnsafe(int price, int quantity);
int placeOrderSafer(struct price, struct quantity);
...
placeOrderUnsafe(quantity.value, price.value) /* does the wrong thing */
placeOrderSafer(quantity, price) /* caught at compile */
Surprising to me to use "the map is not the territory" this way when static typing constrains and makes provable claims about the territory.
If none, or even most of those top 25 errors don't mostly look like type errors to you, you don't know enough about good type systems to be making judgement calls about them.
In my current project (in C), I statically ensure that functions are run on the correct thread. "Oops, that function isn't supposed to be called there because it makes obscure assumptions" is one of the hardest bugs to catch, and my (unsophisticated!) type system regularly catches it for me.
I create a struct representing each thread. Outside of a debug build, these structs are empty. This is always passed as the first argument to any interesting function (as it happens, while the C standard doesn't guarantee it, in GCC this generates the same bytecode as omitting the parameter), and always named th.
When defining any global variable designed to be accessed without a lock, I also create a LOCAL_varname_ASSERT_THREAD function that takes the relevant thread as an argument and does nothing, for static assertion of type equality. This is all wrapped in macros to be convenient and readable.
When you really start using your type system, it's amazing what can be "a type error", even in something as kludgy as C.
At this point, I've been working on the codebase for a year and a half, and it's been in production for much of that. It's >100k LOC, has multiple threads, generates responses in <10us, has been through some major refactorings, and I've had maybe 3 problems involving concurrency that even hit my tests, with one (a high level livelock in my message passing) winding up in production. I don't know how I would have managed this without access to these kinds of static guarantees (which is not to say there aren't any other tools which could have replaced this one, but it is to say there is tremendous value to this tool when you know how to use it!).
This is interesting. Pretty sure I get it but if this is open source I'd like to see it. Two comments:
1) I'm not sure it would be much more effort to implement this scheme in a dynamic language. Most of them can introspect their own code and you could easily flag such an error at startup time.
2) I like the style of passing a thread to every function. In that case, I wonder why you even have globals that multiple threads need to access. What I try to do is initialize ALL shared data in main(). And then pass those structures ONLY to the exact threads that need them. This can be done in either static or dynamic languages; it enforces a nice structure and is easy to read.
I'm not saying a dynamic language would be better for this project. C is a great tool and appropriate for a huge number of problems (also inappropriate for a huge number of problems).
FWIW Ritchie's C (the one they wrote Unix in) was very weakly typed, and that heritage still shows. I don't think it's an accident that C is popular; its type system doesn't get in your way, doesn't bloat your code, and also allows creative use/abuse.
"1) I'm not sure it would be much more effort to implement this scheme in a dynamic language. Most of them can introspect their own code and you could easily flag such an error at startup time."
That's just implementing a static type system in the dynamic language.
"2) I like the style of passing a thread to every function. In that case, I wonder why you even have globals that multiple threads need to access. What I try to do is initialize ALL shared data in main(). And then pass those structures ONLY to the exact threads that need them. This can be done in either static or dynamic languages; it enforces a nice structure and is easy to read."
I code much closer to that when latency matters less. As it stands, reshuffling different views for different functions takes precious nanoseconds every function call.
Edited to add: My response to 1 should not be interpreted as "BAM! Point for statically typed languages!" My contention is that statically checked type systems are phenomenally useful - this really just weakens the notion of static or dynamic types being a fundamental attribute of the language. I think a more accurate perspective is that for any language and any type system, there is some subset of the language that abides by the type system. That intersection may or may not be useful, and may or may not be checkable, but the most joy is to be found where it is both. The only real wins from integration of that checker with the compiler are 1) it's unavoidable (which can be relevant if you generally have sloppy process, but fix your process), and 2) the type information may provide invariants useful for optimization.
I am actually a big fan of statically typed languages. But it's naive to think a type system will make your programs correct by catching type errors. I do believe a type system helps making programs correct as a design aid.
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.
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.
That second problem I summarize using the phrase the "map is not the territory". (http://en.wikipedia.org/wiki/Map%E2%80%93territory_relation) I had heard this phrase for many years, outside the context of programming. I never quite understood what it meant until I spent time around hardcore C++ and Haskell people. Static typing is a model (a map) for runtime behavior.