Yes. That's "design by contract", which is extremely useful for determining who's at fault.
This came out of aerospace, where it's taken seriously. If A won't interoperate with B, you check the interface spec. If A is out of compliance, A has to be fixed. If B is out of compliance, B has to be fixed. If you can't tell, the interface spec has to be fixed. This is why you can unplug Pratt and Whitney engines from an airplane and plug in Rolls-Royce engines.
This worked in the era when the buyer had more clout than the seller. Now, if A won't interoperate with B, it's the problem of whomever is smaller.
> This is why you can unplug Pratt and Whitney engines from an airplane and plug in Rolls-Royce engines.
Wait wut? Are you talking about their embedded software or the hardware itself? Because if you're talking about the hardware, I'm about to be dumbfounded that there are formal verifications of hardware, my mind is about to be blown.
You could think of many of the formal tools outside of dependently typed programming as design by contract plus a thingy that complains if the contract doesn't work.
This came out of aerospace, where it's taken seriously. If A won't interoperate with B, you check the interface spec. If A is out of compliance, A has to be fixed. If B is out of compliance, B has to be fixed. If you can't tell, the interface spec has to be fixed. This is why you can unplug Pratt and Whitney engines from an airplane and plug in Rolls-Royce engines.
This worked in the era when the buyer had more clout than the seller. Now, if A won't interoperate with B, it's the problem of whomever is smaller.