The last ruby project that I worked on laughed at static analysis tools before pitching them into halting problems. You have to execute ruby code just to assemb

The last ruby project that I worked on laughed at static analysis tools before pitching them into halting problems. You have to execute ruby code just to assemble the classes, it's quite resistant to static analysis unless you artificially restrict yourself to a subset of the language. If you're going to limit yourself to the statically checkable part of the language then you might as well just use a language that was designed for it. The fundamental feature of dynamic languages is variations on the theme of self-modifying code - behaviour is determined at runtime. This feature is not normally considered compatible with static analysis, because you have to execute an unbounded amount of the program to find out what it does. The important thing about static type checking on languages like ocaml is that it can be both "sound" and "complete" - any type error is an error in your program, and a program that type checks cannot go wrong according to the constraints of the type system. In order to make this possible, we have a body of theory on how to design type systems that are constrained just enough to be checkable while still expressing everything you want them to say.