Erlang 2024: Proceedings of the 23rd ACM SIGPLAN International Workshop on Erlang

The rising threat of climate change is leading countries to commit to ambitious carbon-reduction goals. Concurrently, a significant portion of Fortune 500 companies are targeting carbon emission cuts by 2030. As digital integration grows, Technology represents a huge opportunity, yet, the energy footprint of software is often overlooked. Each application transaction, interaction and new data asset adds to the energy demand, making sustainable software and data practices crucial. While improving sustainability in data and software alone won’t solve climate change, with an understanding of technology’s contribution to carbon emissions, a focus on tech’s foundational elements at multiple levels can pave the way for more substantial reductions in the future: (i) Software engineers can reduce the carbon emissions from their software and data by being aware of the effects of their choices. (ii) CTOs can make environmental sustainability a non-functional requirement for all software development. (iii) Companies can incorporate the environmental effects of software as a metric when gauging the quality of a solution. The goal is to cultivate a culture that embeds environmental sustainability into standard software and data engineering practices. Now is the perfect time to start!

Erlang is a dynamically typed language with support for optional type annotations. Though Erlang’s type annotations were originally intended for documentation, static analysis tools soon utilized them for semantic checks. The most advanced and mature of these tools is Dialyzer, a success typing-based tool widely used in current projects. Attempts to retrofit a static type system employing the type annotations have so far remained in the realm of research prototypes. Recently, three further tools have been developed: Gradualizer, eqWAlizer, and Etylizer. But, due to a need for more semantic agreement on Erlang’s type annotations, their results differ in ways that can be challenging for users to interpret. In this paper, we cross-compare the state-of-the-art static checkers regarding their expressivity and performance on the union of their respective test suites. Unsurprisingly, we find that the tools perform best on their own test suites. While Gradualizer, Etylizer, and eqWAlizer disagree on 25% - 45% of test cases across all test suites, Dialyzer’s success-typing approach sets it apart in its interpretation of the type annotations. Our analysis emphasizes that the nature of Erlang’s type language remains challenging when it comes to develop a correct and efficient static type checker.

Distributed systems are notoriously difficult to design and implement correctly. Although formal methods provide rigorous approaches to verifying the adherence of a program to its specification, there still exists a gap between a formal model and implementation if the model and its implementation are only loosely coupled. Developers usually overcome this gap through manual effort, which may result in the introduction of unexpected bugs. In this paper, we present Erla+, a translator which automatically translates models written in a subset of the PlusCal language to TLA+ for formal reasoning and produces executable Erlang programs in one run. Erla+ additionally provides new PlusCal primitives for actor-style modeling, thus clearly separating the modeled system from its environment. We show the expressivity and strengths of Erla+ by applying it to representative use cases such as a Raft-based key-value store. Our evaluation shows that the implementations generated by Erla+ offer competitive performance against manually written and optimized state-of-the-art libraries.

Erlang is a functional programming language with structural type-checking. Opaque types are the only types with a nominal component, where their names are used for type-checking. Using opaque types for nominal typing is possible, but it limits the use of pattern-matching and deconstruction to the module where it is defined. To distinguish types by names without imposing extra constraints, we introduce the new concept of nominal types for Erlang, together with a well-tested type-checking implementation in Dialyzer. We define a new syntax for declaring nominal types and a set of rules that specify how nominal types should be type-checked with respect to other nominal types and non-nominal types, which is designed to ensure backwards compatibility. Nominal type-checking is implemented on top of Dialyzer's structural type-checking logic. Through testing in the Erlang/OTP codebase, we show that nominal types can encode Erlang's opaque types, thereby improving Dialyzer's performance and maintainability.

In this work, we consider the formal framework TOAST for timed asynchronous interactions featuring mixed-choice states. TOAST extends the theory of timed asynchronous session types to support modelling of communication protocols featuring timeouts, which despite being commonplace in practice were previously out of reach for session type theory. We present ongoing work towards a practical toolchain that (a) automates the generation of correct-by-construction program stubs with timeouts in Erlang from TOAST processes that implement a TOAST protocol, and (b) provides an inline monitoring framework for TOAST protocols integrated with Erlang supervisors. Our toolchain generates Erlang code with a close correspondence to the source TOAST model by building on a formal correspondence between session types and Communicating Finite State Machines. The monitoring framework can be configured to perform either runtime verification or enforcement with respect to the source protocol, ensuring communication safety.

Erlang is an unorthodox language that has fault-tolerance and observability (tracing) baked into the language. This allows users to debug production systems without the maintenance overhead of adding these features manually, but comes at the cost of adding a side effect to almost every operation. Because the design choices around tracing err on the side of maximum observability, the compiler does not have much freedom to perform common optimizations, and requires sophisticated analysis to safely apply all but the simplest transformations. Each individual optimization also implements its own bespoke analysis, which is error-prone and difficult to maintain. This report describes an ongoing experiment on translating one of the compiler's intermediate representations (IR) to formulas, enabling the use of a satisfiability modulo theories (SMT) solver to drive analysis as well as prove the semantics-preserving nature of optimizations.

We present an automated approach to checking whether a change to a repository is a refactoring, that is, it makes no change to the behaviour of the system. This is implemented in the EquivcheckEr tool, which detects the places in which the code has changed, and compares the old and new versions of all functions that are affected by the change, applying the functions to randomly generated inputs. Our tool works for projects written in Erlang, and so needs to deal with effectful as well as pure functions. We aim only to report inequivalence when we have concrete evidence to that effect, avoiding any ``false positive'' counterexamples.

We describe the design and implementation of Scheduler, a new library for Elixir which provides a user-level scheduler. The goal is to improve the control over scheduling decisions, i.e., which process runs at which time, in order to obtain executions that are more random, but which are also repeatable and modifiable, and which moreover provide a detailed explanation of the scheduling decisions taken. This work is inspired by the Pulse user-level scheduler for Erlang programs, as well as other related tools. Our library is agnostic regarding what other testing/execution/formal verification tool uses the scheduler, and instruments Elixir code running under the scheduler through use of the Elixir macro facility. Moreover, the library provides a number of algorithms to explore the state space of the concurrent programs under study, including random search, depth-first search (potentially capable of exploring the whole state space of the program-under-study), and a novel search algorithm which selects schedules randomly. As an example the Scheduler library is applied to the task of checking whether a number of snapshot algorithms are correct.

In December 2023, security agencies from five countries in North America, Europe, and the south Pacific produced a document encouraging senior executives in all software pro- ducing organizations to take responsibility for and oversight of the security of the software their organizations produce. In February 2024, the White House released a cybersecurity outline, highlighting the December document. In this work we review the safe languages listed in these documents, and compare the safety of those languages with Erlang and Elixir, two BEAM languages. These security agencies’ declaration of some languages as safe is necessary but insufficient to make wise decisions regarding what language to use when creating code. We propose an additional way of looking at languages and the ease with which unsafe code can be written and used. We call this new perspective unsafe impedance. We then go on to use unsafe impedance to examine nine languages that are considered to be safe. Finally, we suggest that business processes include what we refer to as an Unsafe Acceptance Process. This Unsafe Acceptance Process can be used as part of the memory safe roadmaps suggested by these agencies. Unsafe Acceptance Processes can aid organizations in their production of safe by design software.

IoT systems are increasingly pervasive, and developing, maintaining and ensuring the reliability of the software is challenging. IoT software is conventionally structured in multiple distributed tiers, where tiers use different programming languages and components that must interoperate. One way to minimise this complexity is to use a single tierless language to specify the entire IoT system. Tierless IoT languages require extremely sophisticated implementations, and are new and rare. A previous study compared two Clean-based tierless implementations of a smart campus IoT system (CRS and CWS) with two conventional tiered Python implementations (PRS and PWS). It showed that tierless languages dramatically reduce development effort. This paper describes a new implementation of the smart campus system in the Elixir/Potato tierless language (ERS), and compares ERS with the other implementations to show the following. (1) We provide further evidence that using a tierless IoT language reduces development effort. (2) We provide the first ever comparative study of two fundamentally different tierless IoT languages, i.e. we compare Elixir/Potato with Clean/iTask(mTask) using the ERS and CRS/CWS case studies. (3) We provide the first ever analysis of the software engineering costs of providing failure management in a tierless IoT language.

Animal shelters are non-governmental organizations that have to face many difficulties in their management and carry out actions to help unprotected animals in the area. Apart from being small organizations and generally having limited resources, many of them also struggle with outdated tools or face challenges in centralizing their information and pro- cesses. However, the main problem faced by them is related to their economic situation and most of the time they need to use free online tools for their management. This work presents and explains a Phoenix web application solution to assist in the management of these groups, which leverages affordable development and easy maintenance with tailoring to meet their main needs. With this experience report, we aim to demonstrate that BEAM technologies, which have already proven their effectiveness in bigger corporate set- tings, such as WhatsApp or Discord, are also well-suited for smaller and more modest environments. Moreover, this aims to be an example of the use of Elixir/Phoenix in a non-profit environment, typical for social and community projects, with needs specific to the world in which they exist.