The question of computation vs. interaction is an fascinating one, but I think there's another question (perhaps related) to the applicability of "rich" types to practical programming, and that is regarding the role of types, and how far they should be stretched. I think there is little question that "simple" type systems (like in C/C++/Java/C#) aid in developing large systems. But much of the fascination with type t…
> The benefit of proofs in code would only be worthwhile if it was relatively easy for common programmers to prove the absence of bugs that would have been more costly to find and fix using other methods, and that that ease would not come at the cost of other properties (such as performance). I don't understand why proofs need to be universally easy to write/understand to be useful. Why can't they be useful for a sub…
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.