Do these things actually help us develop software at increasingly large scales?
I've always considered the primary purpose of type systems to be restricting how data can flow through a program.
See also "A Perspective on Information-Flow Control": http://www.cse.chalmers.se/~andrei/mod11.pdf
It seems like modeling data flow via messages would be pretty natural semantics for something like this. But first I need to dig into what Hoare logic is and how it applies.
Therefore, I am also a bit dubious about IFC. It seems to me that Data Flow Analysis is more suitable.
We are essentially hinting at the same thing I guess, but I expect some type system tie-ins. Otherwise it might become too abstract.
Perhaps what you're pointing out is that there are many dynamic and static ways to verify assertions about programs? Certainly.
When programmers talk about "type systems" I think they tend to mean a static, sound, computable approach to verifying assertions about programs.
JIF is a _type system_, albeit not a unification-based one like ML. Moreover, the situations the GP is discussing seem like things that don't need the powerful type system of JIF. Something like ML could handle those situations with ease.
I think contract often takes one of two meanings among non-researchers. Either people are referring to assertions that are dynamically checked or they're referring to very expressive assertions (regardless of when they're checked).
These are all different ways of proving statements about programs.