Nine Nines, so much for Intuition

In this specific example, that means 99.9999999 percent reliability, 1.7 million lines of an agile language ("dynamic types") handling 30-40 million calls per week with only 31 milliseconds of downtime per year. The figures are from Joe Armstrong's talk to the Lightweight Languages 2002 conference.

I am reminded of these figures due to a quote...

Mainly, I would want strong type checking in an application which had to run unattended, had to never crash, and had to always be right.

As it turns out, this may be one of the least desirable scenarios for strong typing! So much for intuition.

Later in the comments on that blog...

What we need is for ML, be it O'Caml, SML, or some other variant, to become ridiculously popular. In fact, any language with implicit typing would suffice. Implicit types are the way to go: all the supposed security of statically typed languages, without the feeling you're talking to an autistic child.

This may be. I am interested in these languages, and I've done some toy programming in Haskell and ML. But this claim for what "we need" smells suspiciously untested. I have yet to see evidence on the order of what has been achieved many times in production scenarios with dynamic languages. I remain a fascinated skeptic who would be eager to see real results being reported.

Chris Petrilli adds...

Static typing is simply a false meme promulgated by people who are stuck with it.

Rather than the dubious benefits of static type checking, I believe more effort should be put into dynamic, concurrent model checking. A good introduction using Java is available.

This is the future of "checking" things in programs. Another book I'd recommend is "Logic in Computer Science: Modelling and Reasoning About Systems". The deep reasoning capabilities we should be developing is about the dynamic, concurrent nature of systems.

[T]his material is rarely taught to computer scientists and electrical engineers who will need to use it as part of their jobs in the near future. Instead, engineers avoid using formal methods in situations where the methods would be of genuine benefit...

Logic in Computer Science by Huth and Ryan is an exceptional book. I was amazed when I looked through it for the first time. In addition to propositional and predicate logic, it has a particularly thorough treatment of temporal logic and model checking. In fact, the book is quite remarkable in how much of this material it is able to cover: linear and branching time temporal logic, explicit state model checking, fairness...

The book is a wonderful example of what a modern text on logic for computer science should be like. I recommend it to the reader with greatest enthusiasm...

Adding static types to Python should be the last thing on the list to do.