The circularity-argument for type systems is actually correct, but that is an aside. Type systems on programming languages are proof systems, so they can be use

The circularity-argument for type systems is actually correct, but that is an aside. Type systems on programming languages are proof systems, so they can be used as tools for building better type systems. There is a big lack of TDD in highly succesful Open Source endeavors. Part of this is perhaps because a failed project never get attention. But also note that defects in Open Source projects are good. They instill new programmers to come to the project and work on it because there are some easy low-hanging fruit. Furthermore, as exemplified by Keith Packard recently (see http://lwn.net/Articles/354408/ http://lwn.net/Articles/354408/ -- which unfortunately is behind the Iron Curtain for 24 hours more). Keith mentions that he sometimes deliberately breaks some old code by introducing obvious bugs into it. Then, when nobody have complained for a couple of years, it can be removed on the grounds that it was not interesting. With rigorous testing this is unachievable.