By the way, I am currently doing a literature study into type theory for my study and I was annoyed by the lack of introduction material for programmers wanting to learn more about it. I've been thinking of writing a "Type theory from first principles for dummies" but I was unsure how much interest there'd be in something like that. If you (or other people here on HN) would be interested in that let me know...
I think that would be a very valuable article. Right now people are basically stuck with TAPL [1], which (while being a fantastic book) is pretty meaty and not exactly cheap. I've been examining the type theory literature myself over the last couple of months (admittedly more from a mathematical angle than a programming one), and there is definitely a dearth of good introductory material. Girard's Proofs and Types is a great book, but it's not easy going and doesn't have a huge amount of direct relevance to programmers. In case anyone else is interested (merijnv, I assume you've glanced at all of these) I have a small bibliography of type theory books [2].
I'm also currently interested in this area, and I would recommend Interactive Theorem Proving and Program Development. At the same time, it is practical and theoretical.
Adam Chlipala's 'Certified Programming With Dependent Types' is a textbook about practical engineering with the Coq proof assistant. The focus is on building programs with proofs of correctness, using dependent types and scripted proof automation:
