While working on my otel presentation for tomorrow:

It turns out that proofs in formal verification and context propagation in distributed tracing have the same problem:

In verification, the shape of a proof eventually ends breaking due to semantically equivalent code changes affecting some internal implementation detail.

In context propagation, libraries end up breaking APIs when they try to expose tracing information for the same reason: The tracing structure becomes semantically relevant.