The author is obviously a fan of B&D languages. (http://catb.org/jargon/html/B/bondage-and-discipline-languag...) There's nothing wrong with preferring a little B&D, but it's a shame that there are still masochists in this day and age that claim other languages are "broken" because they don't spank you often enough.
I don't think that's quite it. The author seems to like languages that let programs be as close to provably correct as possible. He also admits that, for some problems, this is a mistake.
I used to hate static typing with a passion, and I'm still a pretty big Lisp fan, but I've recently taken up Haskell. Many of the examples in this post use Haskell as an example of the right thing, and I'm really starting to see the advantages. Certain common errors are caught by the compiler, and impure operations show up in a function's type signature, reducing the chances of any spooky action at a distance.
Ultimately, I think there's a tradeoff between flexibility and correctness. How much of each to choose depends on the parameters of the project. Some languages try to allow a choice, especially with regard to typing discipline. Haskell offers Data.Dynamic. Common Lisp has optional type declarations and compiler warnings for obvious type errors. There's a post about formalizing such things as "gradual typing" (http://news.ycombinator.com/item?id=556794).
There are reasons why compilers for static languages complain so much for those uneducated in their type systems: because the constructs they are rejecting have, on balance, been determined to be unsound by the languages' designers.
And most of the time, these decisions are correct. In each language, however, there are usually a few exceptions, most of which are the result of learning over time. For example, Pascal over-uses nominal type equality, which is particularly pernicious with arrays, and, in classical Pascal, strings (fixed-length arrays of chars).
And in Java, requiring most possible exceptions to be part of the interface specification is a flaw resulting from a misunderstanding about exceptions: Java seems to feel that no exception should be ignored, while they should actually almost never be caught.
And then there are abhorrences like C++, where historical forces have combined to give the language user more power than they can comfortably wield, or can be comfortably implemented in any given compiler.
Even though it was never mentioned, I couldn't shake the feeling that he was talking about Scala. Scala allows nulls for compatibility with Java, but prefers the statically checked Option type (equivalent to Haskell's Maybe). It puts variables (var) and final variables (val) on equal syntactic footing, but convention dictates you use a val by default and only switch to var if it's really necessary. Case classes and pattern matching let you define statically checked data types. Type inference helps so that all the static typing doesn't get in your way, but errors are still caught at compile time.
Here we hit against a law of nature: there is no algorithm that would analyze an arbitrary piece of code and determine whether it will only produce valid search trees.
Why not? I know about the Halting problem, but I don't see how this is equivalent... am I missing something?
In order to produce a valid search tree, the code must halt. Therefore, an algorithm that can tell whether an arbitrary piece of code will produce valid search trees can tell whether that piece of code will halt.
This isn't really a good example though, because it's quite possible to examing an arbitrary piece of code and, assuming it halts, determine whether it will produce valid search trees. The Haskell and ML typecheckers are existence proofs for this, as is the static typechecker that Wadler did as a bolt-on addition to Erlang.
More practically, the "arbitrary piece of code" can be expressed in a less-than-turing-complete language or language subset, and it would actually be possible to prove useful things about it.
It is a classic diagonal argument. Suppose algorithm P determines whether a given algorithm produces a valid search tree. Consider the following algorithm Q: "if P(Q) the produce invalid tree else produce valid tree." In words, the algorithm Q does the opposite of what P predicts. Such Q exists by Kleene's Recursion Theorem (or simply because you can write its code in your favorite language).
