Those sound like jobs amenable to design by contract and information flow control, not necessarily type systems and type theory, per se (though there is some overlap).
Type Systems, Contract Systems, and IFC are three terms that I think are hard to distinguish using lay language.
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.
IFC is orthogonal to type systems, having also been modeled in terms of axiomatic semantics (Hoare logic) independent of a type system. It can also be practically implemented through runtime monitoring, partial evaluation and various hybrid approaches. Type systems are certainly one way of providing foundations for IFC, but few languages have it as a first-class construct. Notable exceptions are SPARK (based on Ada) and Jif (based on Java).
Interesting, I'll definitely have to check this out. Any input on whether this has been applied and/or could be applied to actor paradigms of computation?
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.
