The point is trust and typing seem orthogonal. E.g. I use static typing within one 'program' but 'dynamic' as soon as I split my program into two, even when the

The point is trust and typing seem orthogonal. E.g. I use static typing within one 'program' but 'dynamic' as soon as I split my program into two, even when the level of trust didn't change. Same thing when including my colleagues' code within my 'program' vs. calling it across program boundaries. The point I'm trying to make is that 'static-typing style verification' which happens across different parts of a 'single program' doesn't extend to multiple programs or real systems. Maybe we should look at some kind of late bound dynamically bound verification - i.e. a protocol that is executed whenever one 'program' reaches out and connects to another, to determine if the connection is safe and correct. Do you think this has value?