Every time I see this claim, I wonder what the heck people are working on that is so simple that getting the types right is all it takes to get the code right? Is it just that enough of my work is math or parsing, both of which typically have an infinite number of ways to get things wrong but with the correct types?
Or is the idea really the other way around -- if your program is sufficiently complex, you'll never get it to actually pass Haskell's type checks?
Edited to add, I love the article you linked to so far. :)
Sometimes I got a type error from some bizzare syntax mistake, usually failing to correctly delineate an expression, and sometimes the algorithm in my head was just wrong and I had to fix it. At that point, the cycle starts over, and the same benefits I mentioned above help in debugging. FWIW, the problem I was working on was fairly simple, but novel. I was a very happy camper this Christmas, working with OCaml, despite its syntax.
Out of curiosity, what language do you do your "math and parsing" in? OCaml might be a good fit.
To give a somewhat extreme example of the sort of stuff I do -- one of my current projects is to try to create a first-class fillet surface type [1] for the geometry engines I work with. My current code converts each fillet to a NURBS surface, but this is slow, consumes a lot of memory, and produces surfaces which frequently are not accurate enough for my purposes. So my hope is to be able to directly calculate points on the fillet and their derivatives.
It's easy enough to calculate points on the fillet surface, but I don't see any obvious way of directly calculating the derivative along the surface. So I've been investigating Chebyshev polynomials in two variables. But that algorithm looks a bit hairy, and I don't have any feel for whether it will be an actual improvement in practice. (And having written all this, I'm suddenly wondering if I'm making every effort to sort out the simple cases that are easy to solve exactly.)
My point here is that figuring out the correct types involved seems like a tiny, tiny part of the required work. Maybe it's because I haven't put in enough time in Haskell, but I don't see how stricter than C++ types are going to help. The real work is getting the math correct and fast enough to be useful.
By the way, my comment is not meant to be a dig at Haskell (et al). I'm not sold on it as a language, but it certainly has a lot of interesting ideas -- pattern matching and laziness spring to mind.
For domains outside of physics and applied math, I think the dominating factor is often the inherent trickiness of writing correct procedural code vs. the ease of writing strongly typed functional code.
Pattern matching is at least as much fun as it looks like, if you have complicated data types. That's a lot of what made OCaml so perfectly match my problem.
[0] https://github.com/andrewf/apatch if you're curious. The meat is in patch.ml
Why can't Lisp do this? In the Common Lisp world, there's some pretty aggressive, though still optional, static type checking. There's also Qi, Shen, Typed Racket, et cetera. The question is orthogonal to the question of syntax.
For example, how would you type the cons function? In Haskell, it has type t -> [t] -> [t] (i.e., for all types t, given a value of type t and a value of type list of t it produces a value of type list of t). In Lisp, on the other hand, you can construct a cons cell out of any two objects.
Obviously you can certainly construct a type system in which you can handle Lisp cons cells reasonably; Hindley-Milner type systems aren't the only game in town. But I don't think it'd have the 'if it compiles it probably works' property any more.
Type systems fall squarely in the "semantics, not syntax" department.
In terms of syntax, I think there's a divide between the needs of static type-systems, versus dynamic ones. LISP is at its core a dynamic language. It makes sense to treat code as being data that can be manipulated. Getting rid of all that syntax gives you great power in terms of what you can do. And personally I find Clojure code to be much saner than code written in Ruby or Python, but that's another discussion.
However, the other side of the coin are Haskell or Miranda (its predecessor) or languages in the ML family or Scala. These languages go to great length to achieve much of LISP's expressiveness, while ensuring a great amount of static type-enforcement. Haskell is especially notable because Haskell is lazy and has many goodies, such as type-classes or rank-2 types. People say that when a piece of Haskell code successfully compiles it is usually correct. LISP can't do this, even though there have been experiments with pluggable type-systems.
For an excellent rant on the choice of Scheme for SICP (and not Miranda, Haskell's predecessor), checkout: http://www.cs.kent.ac.uk/people/staff/dat/miranda/wadler87.p...
So IMHO, syntax helps if you want static type-safety, because the language and the type-system exposed need to be expressive. Whether static type-safety is useful or not, it's a matter of debate, being highly dependent on the problem domain. One could argue that static type-safety is very useful if the shape of the data you're manipulating is well defined and doesn't change much, otherwise you're better off with a dynamic language, but that's another discussion.