Strong typing vs Strong testing refute

Bruce Eckel writes about strong typing vs strong testing – a topic close to my heart. But he makes the common mistake of reducing “runtime typing vs. static typing” to a language feature comparison. Java is a very poor example of static typing!

But I think I disagree with his larger point – that you’re better off with test systems rather than type system. I think you should have both! At work, I’ve watched large programs being built up and I think you reap great benefits from static typing. For a start, types act as documentation. The type of a function argument indicates how it’ll be used. Abstract interfaces act as barriers to complexity within a large system. Type annotations such as ‘const’ in C++ allow you to express some of the semantics of the system and the compiler will check all of your code for violations.

Can tests ever replace this? I think not. Firstly, in my experience, checking enough of the cases is hard. And the cases which don’t get tested are probably the rarely executed ones where bugs lurk. What happens if someone trips over the network cable as your program is sending data? Does that error handler work? How about if the harddisk is full and your program can’t write a temporary file?

Sure, static type systems can’t check very many properties of your program – that’s why I still love unit tests – but they can check quite a lot including a lot of common mistakes. Given that it takes a compiler a few milliseconds to type-check a function I think static typing is a big win. The compiler won’t suffer from deadline stress and forget to check your new code.

I wonder if many of the great claims made about programs written in python arise from people who don’t write very large systems, and who don’t have to be very strict about dealing with every single failure condition. It’s one thing for bittorrent to fall over when something goes bad. It’s quite another if software in a life-support system bails.

I see things like ‘const’ in C++ and I wonder if there are other annotations which I could add to my source code, so that they act both as documentation of my intent and so that the compiler will check them. This is what lead me to my current fascination with computer languages and their facilities. I talked to Anthony about this a while ago, since he did his PhD on something-to-do-with-type-systems and he murmed in a “it’s tricky” way. Around that time, I looked at dependent types. With this more powerful type system you can express stuff like “foo() is a function which takes two arguments: a vector of integers called ‘data’ and an integer called ‘length’ but furthermore the vector will always have that length”. But, apparently that makes the type system undecidable in general. In plain english, your compiler can say “your program is well-typed” or “there’s a type error” or it could go into a loop trying to decide. That’s not great and I find it a bit worrying that something which can be expressed so simply in english messes up your compiler so bad.

But, hey, even I have doubts. Not because I feel shackled by the type system in ocaml or haskell but because systems like Squeak have much better tools for exploring and tweaking systems. Hmm ….