Choreographic programming is a paradigm where developers write the global specification (called choreography) of a communicating system, and then a correct-by-construction distributed implementation is compiled automatically. Unfortunately, it is possible to write choreographies that cannot be compiled, because of issues related to an agreement property known as knowledge of choice. This forces programmers to reason manually about implementation details that may be orthogonal to the protocol that they are writing. Amendment is an automatic procedure for repairing uncompilable choreographies. We present a formalisation of amendment from the literature, built upon an existing formalisation of choreographic programming. However, in the process of formalising the expected properties of this procedure, we discovered a subtle counterexample that invalidates the original published and peer-reviewed pen-and-paper theory. We discuss how using a theorem prover led us to both finding the issue, and stating and proving a correct formulation of the properties of amendment.

翻译：编舞编程是一种编程范式，开发者编写通信系统的全局规范（称为编舞），然后自动编译出正确性自带的分布式实现。然而，由于与称为"选择知识"的一致性属性相关的问题，编写无法编译的编舞是可能的。这迫使程序员手动推理可能与所编写的协议正交的实现细节。修正是修复不可编译编舞的自动过程。我们基于现有的编舞编程形式化方法，提出了文献中修正的形式化方案。然而，在形式化此过程的预期属性时，我们发现了一个微妙的反例，使得已发表并经同行评审的原始纸质理论失效。我们讨论了如何使用定理证明器不仅发现了问题，还陈述并证明了修正属性的正确表述。