I work at an e-commerce company. I was thinking today of how typed programming would make our code more reliable, and I began to wonder about using types (or other static assurance methods) to ensure that we don't accidentally reveal information to parties that shouldn't see it. I'm thinking here of the Apollo project (specifically, Translating dependency into parametricity) or Flow Caml. I don't see a way for us to use technology like this when working with other companies.
As an example, we might pass a customer's info to a third party site along with some identifying informaiton about us, to verify the third party that the customer is legit. How can I trust the third party site to not reveal our shared secret to the customer?
I suspect this is a problem for cryptographers, not type theorists. Since much of the information that we deliver to customers is tainted by using secrets to obtain it, static analysis wouldn't help maintain security.