In the paradigm of choreographic programming, the overall behaviour of a distributed system is coded as a choreography from a global viewpoint. The choreography can then be automatically projected (compiled) to a correct implementation for each participant. This paradigm is interesting because it relieves the programmer from manually writing the separate send and receive actions performed by participants, which simplifies development and avoids communication mismatches. However, the applicability of choreographic programming in the real world remains largely unexplored. The reason is twofold. First, while there have been several proposals of choreographic programming languages, none of these languages have been used to implement a realistic, widely-used protocol. Thus there is a lack of experience on how realistic choreographic programs are structured and on the relevance of the different features explored in theoretical models. Second, applications of choreographic programming shown so far are intrusive, in the sense that each participant must use exactly the code projected from the choreography. This prevents using the code generated from choreographies with existing third-party implementations of some participants, something that is very beneficial for testing or might even come as a requirement. This paper addresses both problems. In particular, we carry out the first development in choreographic programming of a widespread real-world protocol: the Internet Relay Chat (IRC) client--server protocol. The development is based on Choral, an object-oriented higher-order choreographic programming language (choreographies can be parametric on choreographies and carry state). We find that two of Choral's features are key to our implementation: higher-order choreographies are used for modelling the complex interaction patterns that arise due to IRC's asynchronous nature, while user-definable communication semantics are relevant for achieving interoperability with third-party implementations. In the process we also discover a missing piece: the capability of statically detecting that choices on alternative distributed behaviours are appropriately communicated by means of message types, for which we extend the Choral compiler with an elegant solution based on subtyping. Our Choral implementation of IRC arguably represents a milestone for choreographic programming, since it is the first empirical evidence that the paradigm can be used to faithfully codify protocols found `in the wild'. We observe that the choreographic approach reduces the interaction complexity of our program, compared to the traditional approach of writing separate send and receive actions. To check that our implementation is indeed interoperable with third-party software, we test it against publicly available conformance tests for IRC and some of the most popular IRC client and server software. We also evaluate the performance and scalability of our implementation by performing performance tests. Our experience shows that even if choreographic programming is still in its early life, it can already be applied to a realistic setting.

翻译：在编舞编程范式中，分布式系统的整体行为被编码为从全局视角出发的编舞（choreography）。该编舞随后可自动投影（编译）为每个参与者的正确实现。这一范式之所以引人注目，是因为它免除了程序员手动编写参与者所执行的独立发送和接收动作，从而简化开发流程并避免通信不匹配问题。然而，编舞编程在现实世界中的适用性仍尚未得到充分探索。其原因有二：首先，尽管已有多种编舞编程语言被提出，但这些语言均未被用于实现真实且广泛使用的协议，因此缺乏关于实际编舞程序结构以及理论模型中不同特征相关性的经验；其次，当前展示的编舞编程应用具有侵入性，即每个参与者必须严格使用编舞投影生成的代码。这种特性阻碍了将编舞生成的代码与某些参与者的现有第三方实现结合使用，而后者在测试中极具优势甚至可能成为硬性要求。本文同时解决了这两个问题。具体而言，我们首次实现了基于编舞编程的广泛真实世界协议——互联网中继聊天（IRC）客户端-服务器协议。该实现基于Choral——一种面向对象的高阶编舞编程语言（编舞可参数化于编舞并携带状态）。我们发现Choral的两项特性对实现至关重要：高阶编舞用于建模因IRC异步性而产生的复杂交互模式，而用户可定义的通信语义则对实现与第三方实现的互操作性具有关键作用。在此过程中，我们还发现了一个缺失环节：通过消息类型静态检测分布式备选行为的适当通信能力。为此，我们基于子类型机制为Choral编译器扩展了一种优雅的解决方案。我们的Choral实现的IRC协议堪称编舞编程领域的里程碑，因为它首次提供了实证证据，证明该范式可用于忠实编码"野外"环境中存在的协议。我们观察到，与传统编写独立发送和接收动作的方式相比，编舞方法降低了程序的交互复杂度。为验证实现与第三方软件的互操作性，我们针对IRC的公开一致性测试以及最流行的IRC客户端和服务器软件进行了测试。我们还通过性能测试评估了实现的扩展性和性能。经验表明，尽管编舞编程仍处于早期发展阶段，但已可应用于真实场景。