After trying to read up about dependent types and their relationship to subtypes, I've realized that any paper which starts off with "we /discuss|prove|demonstrate/" is pretty much useless to the average programmer. I would love to see more papers aimed at people who don't have a strong comp-sci background.
