They can, but that would hardly make a deep impact on the industry. And my question would then be why do you think they'll be useful only for a subset of programmers and a subset of projects?
> Types can be used to encode complicated invariants of software systems, which will be automatically be machine checked throughout the entire lifetime of your project.
I know they can, but so can other verification mechanisms that are less intrusive, or even pluggable types, like those that have recently been added to Java 8.
One point of difficulty -- that the article is talking about -- is precisely those variants that are really hard to enforce, like "every request X will be handled within 300 ms", or "the server will never respond Y if the user has never asked for Z", or "the system will never contact the database if the operator has turned on the offline flag". Similar (though less sophisticated) kinds of guarantees are made and verified by Esterel, without requiring the programmer to supply the proof. Other approaches include behavioral programming[1] (made by the same people behind the research that had led to Esterel), which simply let you specify a rule: "if offline flag is on, disable calls to the database", which will be enforced no matter how much lower priority rules try to access the database.
Types are just one approach for verification. There are invariants they excel at proving, and those that not so much. People who research type systems should, of course, explore anything that's possible with them, but software developers should realize that types are not the be-all and end-all of writing verifiably correct programs, and that for some program properties there are better approaches than types.
> They model invariants, help design and allow easy reasoning over large software projects.
I agree in theory. But I also think they may help up to a certain point and then start hurting. The problem is, this has never been put to the test.