> If you want a property to uphold, formulate it as a type. The compiler verifies. Consider two issues with this: 1. How do you verify that the property to u

> If you want a property to uphold, formulate it as a type. The compiler verifies. Consider two issues with this: 1. How do you verify that the property to uphold is indeed the same as formulated by the type? This is easier for simple types, but can get complicated real fast once you start getting into higher kinded types. Ideally you want the 'formulation' of the 'property to uphold' to be specified in the domain of the problem itself. 2. The compiler can only verify what it builds - but we don't build and deploy large systems all at once. We just build and deploy one subsystem - i.e. a single program at a time - into an already running system. So what about verification for coupling between different programs? (The Internet is dynamically typed). To solve #2, we might need some kind of run time negotiation and verification (and once you have that, perhaps it can that be used within each 'program' as well?).