From if to verify: How to Actually Teach Erlang (from Refactoring to Actor System Verification)

Teaching Erlang is easy. The hard part is getting students to think in Erlang.

Anyone who has taught functional programming to students coming from C, Java, or Python knows the obstacle: the student writes Erlang with a Java accent. They use commas as statement separators, if as a control-flow construct, temporary variables for everything, and at the end they ask: “Professor, why doesn’t this feel functional?”

The paper “Modern Erlang Teaching from Code Refactoring to Actor System Verification” by Sergey Staroletov (Polzunov Altai State Technical University), presented at the Erlang Workshop 2026 (co-located with ICFP), synthesizes years of experience teaching Erlang in a Master’s program in Software Engineering and proposes a methodological progression that goes from refactoring imperative code all the way to formal verification of actor systems with Promela/SPIN.

In this article, I’ll break down that progression and show why it works in practice.

The problem: the “imperative accent” in Erlang code

The typical Erlang student already knows how to program in imperative languages. They are used to sequential execution, mutable state, and explicit control flow. When they write Erlang, they reproduce those patterns:

process_one(Parent, [First|Next]) -> FullName = Parent ++ "/" ++ First, IsDir = filelib:is_dir(FullName), if IsDir == true -> recurser(FullName); IsDir == false -> io:format(FullName ++ "~n"), process_one(Parent, Next) end; process_one(_, []) -> ok. 

This code works, but it violates the principles of functional style: there are commas separating “commands,” an imperative if, and temporary variables that create hidden temporal dependencies. The compiler cannot safely reorder those expressions, and the student does not see the benefits in parallelization and testability that the functional paradigm offers.

Staroletov’s proposal is to systematically refactor this code until commas as sequential operators are eliminated and replaced by function composition.

Step 1: Refactoring — eliminate the commas

The goal is to transform the body of each function into a single expression, composed of calls to smaller functions.

The methodology has five steps applied to the original code:

1. Isolate side effects (I/O, process dictionary access, file writes).
2. Introduce intermediate functions for each expression evaluated sequentially.
3. Pass the result of the previous evaluation as a parameter to the next function, instead of storing it in a temporary variable.
4. Replace if with pattern matching (different function clauses for different guards or types).
5. Eliminate code duplication by moving repeated computations into separate functions and then composing them.

Applied to the example:

%% Step 1: isolate construction of the full name construct(Parent, First) -> Parent ++ "/" ++ First. %% Steps 2 and 3: eliminate FullName and IsDir by passing the result forward process_by_dir(true, FullName) -> recurser(FullName); process_by_dir(false, FullName) -> io:format(FullName ++ "~n"). %% Step 4: pattern matching instead of if process_construct(Parent, First) -> Full = construct(Parent, First), process_by_dir(filelib:is_dir(Full), Full). %% Step 5: compose everything process_one(Parent, [First|Next]) -> process_construct(Parent, First), process_one(Parent, Next); process_one(_, []) -> ok. 

The final code is a chain of compositions and accumulator recursion. There are no commas separating “commands” — only expressions that compose.

Why does this work pedagogically? Because the student sees the transformation happen. They do not receive a ready-made solution; they refactor the code they wrote themselves, step by step, until the functional style emerges naturally.

Step 2: Recursion with Taylor series — breaking the factorial/Fibonacci mold

After refactoring, the next challenge is recursion. The classic examples — factorial, Fibonacci, list sum — are useful, but they do not reveal the depth of recursive thinking.

Staroletov proposes computing sine via the Taylor series (Maclaurin):

[
\sin x = x - \frac{x^3}{3!} + \frac{x^5}{5!} - \frac{x^7}{7!} + \dots
]

The student implements a recursive function that accumulates two parameters: the partial sum and the current term, with two stopping criteria — precision (\epsilon) and a maximum number of iterations.

sin_n(X, Sum, Current, I, IMax, EPS) when IMax > 0, abs(Current) < EPS -> Sum + Current; sin_n(_X, Sum, Current, I, IMax, _EPS) when I >= IMax -> Sum + Current; sin_n(X, Sum, Current, I, IMax, EPS) -> sin_n(X, Sum + Current, Current * (-1.0 * X * X / ((2 * I) * (2 * I + 1))), I + 1, IMax, EPS). sin_e(X) -> sin_n(X, 0.0, X, 1, 100, 0.00001). 

This activity forces the student to:

• accumulate more than one parameter (sum and current term), expanding the concept of an accumulator;
• compute the recurrence factor correctly;
• handle two stopping criteria (protection against divergent series);
• understand numerical limitations (for large (|x|), the series converges slowly, requiring argument reduction).

The method is reinforced with other problems that use the same scheme — computing (\pi), computing (e), manipulating lists without using the ready-made functions from the lists module — and each function must be accompanied by unit tests with EUnit.

Step 3: Lightweight processes — the “wow” that changes perspective

After consolidating the functional core, the course introduces the actor model. The paper highlights an impactful demonstration: a TCP server in Erlang that handles thousands of simultaneous connections on modest hardware, briefly compared with modern Java virtual threads.

The pedagogical point is the order of magnitude: Erlang processes use about 326 words of memory (2.6 KB on 64-bit), versus 1–8 MB per operating-system thread. The BEAM scheduler runs in user space, preempting processes based on reduction counts. The student sees in practice why the actor model scales where traditional threads collapse.

Step 4: Verification — Promela as a logical continuation of the actor model

Here is the most interesting methodological differentiator in the paper. Instead of treating formal verification as a separate and “scary” topic, Staroletov presents it as a natural continuation of studying actors.

The idea is simple: if the student already thinks in terms of processes, channels, and message passing, they already have the mental framework to model those same concepts in Promela and verify them with SPIN.

The mapping is almost direct:

• Erlang processes → Promela processes;
• PIDs → dedicated channels between processes (since Promela has no direct equivalent to PIDs);
• message send/receive → channel operations (! and ?).

The student formulates LTL properties and verifies them in SPIN. The basic set includes:

SPIN builds the automaton and returns either “no errors” or a counterexample with the sequence of transitions that violates the property. The classic teaching example is a modified ping-pong: the Pong process sends a request to the Right process before replying, but Right “forgets” to respond. The property “every ping results in a pong” is violated, and the counterexample shows Pong waiting forever.

The student then sees the bug happen in the simulator — and understands why verification is not an academic luxury, but part of engineering culture: “it is not enough to write the system; you must analyze it and prove its properties.”

Step 5: The end-to-end lab — a system that evolves

All these topics are not isolated exercises. The course ties them together in a single lab cycle, in which students develop the same distributed system throughout the semester:

1. They start with simple processes;
2. Evolve to OTP supervision;
3. Integrate Java via JInterface (to demonstrate the contrast between Erlang’s declarative style with pattern matching and Java code loaded with object transformations);
4. Add a case study of a simplified PoET consensus protocol;
5. Verify the model in Promela/SPIN;
6. Optionally port it to Cloud Haskell.

This continuity is powerful: the student does not see “refactoring,” “recursion,” “actors,” and “verification” as disconnected subjects. They see a system growing — and each new technique solves a real problem that emerges from that evolution.

Bonus: Erlang in the age of generative AI

The paper also addresses a contemporary challenge: how do you teach programming when the student can ask ChatGPT for code?

Staroletov’s answer is methodological, not prohibitive: live coding and incremental code construction as a counterpoint to the uncritical use of AI-generated code. The student needs to see the code being built, understand every transformation, every design decision, every refactoring. The focus is not the final product, but the reasoning process that leads to it.

Interestingly, verification in Promela benefits from this as well: even if the student uses AI to translate Erlang code into Promela, they still have to do the manual work of defining LTL properties, interpreting counterexamples, and adjusting the model. AI can accelerate the mechanical part, but it does not replace engineering judgment.

Conclusion: a progression that respects the student’s cognition

What makes this approach remarkable is not only the content — refactoring, Taylor series, lightweight processes, Promela — but the order in which everything appears. Each stage prepares the cognitive ground for the next:

• Refactoring eliminates the imperative habit and forces the student to think in terms of composition.
• Mathematical recursion expands the repertoire beyond trivial examples.
• Lightweight processes provide the practical reward: “look at what this model enables.”
• Verification in Promela crowns the structure: the student discovers that they can prove properties about the system they built.

It is a progression that goes from “how to write” to “how to think,” and from “how to think” to “how to guarantee it is correct.”

For anyone teaching Erlang — or any functional language with an actor model — Staroletov’s paper is essential reading. Not because it presents new tools, but because it organizes decades of pedagogical wisdom into a coherent path, tested in the classroom and grounded in the cognitive reality of students.

Main reference: STAROLETOV, Sergey. Modern Erlang Teaching from Code Refactoring to Actor System Verification. In: Proceedings of the 25th ACM SIGPLAN International Workshop on Erlang (Erlang ‘26), 2026. DOI: 10.1145/3830434.3830946

If you have ever taught Erlang (or learned it), what was the biggest cognitive “click” in your journey? Let me know in the comments.