In my view, contracts can do the "redundancy" thing much better than typing can. It's explicit, it's optional, it's a better guarantee that you're getting what you want, it's more flexible, etc. Contracts and TDD are my favorites right now, i guess.

TDD is particularly great, though, as it's an in-code description of what the program should do. If it doesn't pass the tests it doesn't do what you thought it should do--ie, there are bugs.

(Of course, then we have to figure out how to write the tests... but hey...)