Value independence is enormously beneficial for reasoning about software systems at scale. These benefits carry over into the world of formal verification. Reasoning about programs algebraically is a simple affair in a proof assistant, whereas programs with unconstrained mutation necessitate much more complex techniques, such as Separation Logic, where invariants about memory safety, aliasing, and state changes must be established by manual proof. Uniqueness type systems allow programs to be compiled to code that uses mutation for efficiency, while retaining a semantics that enjoys value independence for reasoning. The restrictions of these type systems, however, are often too onerous for realistic software. Thus, most uniqueness type systems include some "escape hatch" where the benefits of value independence for reasoning are lost, but the restrictions of uniqueness types are lifted. To formally verify a system with such mixed guarantees, the value independence guarantees from uniqueness types must be expressed in terms of imperative, mutable semantics. In other words, we ought to express value independence as an assertion in Separation Logic.

翻译：值独立性对于大规模软件系统的推理具有巨大益处。这些优势同样适用于形式化验证领域。在证明助手中，以代数方式推理程序是简单直接的，而具有无约束可变性的程序则需要更复杂的技术，例如分离逻辑——其中关于内存安全、别名和状态变化的不变量必须通过手动证明来建立。唯一性类型系统允许将程序编译为利用可变性提升效率的代码，同时保留具备值独立性的语义以支持推理。然而，这些类型系统的限制对于实际软件往往过于严苛。因此，大多数唯一性类型系统都包含某种"逃生舱口"机制：在放弃值独立性推理优势的同时，解除唯一性类型的限制。要形式化验证这种混合保证的系统，必须基于命令式可变语义来表达唯一性类型所保证的值独立性。换言之，我们应当将值独立性表述为分离逻辑中的断言。