[neilparikh]

I think that mostly works, but it's still possible that different tools assign different semantics for the same syntax, which could then interact in a weird way if the library author wrote the interface annotations with Tool A's semantics in mind, while you ended up checking them against your code with Tool B.

I think the type systems are simple enough that this is probably a theoretical concern, and won't come up often in practice.