Yes, theorem-proving stuff sounds very clever, but no one said that it is at the cost of inability to make a heterogeneous list or even have tuples of different kind in it.) It is, perhaps, possible to prove lots of theorems about very restricted code, I have no idea.
Static analyzers exist for many languages. Clang toolset has a nice one.
As for testing, keeping functions small and doing just one thing will keep amount of tests small-enough.
Let's say that systematic approach of HtDP/Racket guys allows you write decent programs without necessity of proving any theorems about it.)
Yes, theorem-proving stuff sounds very clever, but no one said that it is at the cost of inability to make a heterogeneous list or even have tuples of different kind in it.
That's because that cost isn't actually necessary, it's just Haskell being Haskell. There are plenty of other languages with different type systems that allow for heterogeneous lists very easily (for example, Scala will let you write List[Any] and it will type-check). And some of us research guys are trying to make advances in this stuff (I actually have to email someone to talk about a paper somewhat related to this).
Extensible heterogeneous lists are hard in Haskell, but that's because Haskell chooses to encode extensibility through type-classes rather than data heterogeneity.
It could very well be that most programmers just don't like programming that way, and thus Haskell sucks.
Not really. Just make your types instances of Typeable and then store them in a list of Dynamics. This gives you dynamic typing for those exceptionally rare occasions when you really need it.
Frankly, from my experience with dynamically typed languages such as Clojure few people actually make heterogeneous lists and vectors beyond a handful of elements; a use case which is covered nicely by Haskell's tuples. Long hetereogeneous lists and vectors are not particularly useful because they cannot be reduced/folded -- unless your reducing function accounts for all the different types but then why not use an algebraic data type with pattern matching?
Static analyzers exist for many languages. Clang toolset has a nice one.
As for testing, keeping functions small and doing just one thing will keep amount of tests small-enough.
Let's say that systematic approach of HtDP/Racket guys allows you write decent programs without necessity of proving any theorems about it.)