---
title: "Expressiveness proof"
description: "Dex has a computer-checked proof of what it can express."
canonical_url: "https://docs.superdurable.io/correctness-and-expressiveness/expressiveness-proof/"
source: "docs/content/correctness-and-expressiveness/expressiveness-proof.mdx"
locale: "en"
---
# Expressiveness proof
Dex has a computer-checked proof of what it can express.
- [Download the paper (PDF)](https://docs.superdurable.io/papers/dex-expressiveness.pdf)
- [Formal sources on GitHub](https://github.com/superdurable/dex/tree/main/formal)
## The claim
The paper defines a small concurrent language. It has the usual tools of
concurrent programming:
- threads, with **fork** and **join**;
- shared variables, local variables, and procedures with recursion;
- mutexes and condition variables;
- timers: **sleep**, and a **select** that waits for a message or a timeout;
- cancellation of a thread;
- exceptions;
- external effects, such as sending an email;
- program exit.
The claim: every program in that language translates into a Dex Flow that
behaves the same, seen from outside. The paper states the exact conditions.
"Behaves the same" has two parts.
- **The same events.** Any sequence of events the program can produce, the
Flow can produce, and the other way around.
- **The same ending.** The program and the Flow complete, get stuck, or keep
running in the same situations.
"Seen from outside" means the inputs, the external effects, and the result.
The Flow's internal Channels and Attributes do not count.
## Why it matters to you
Dex has no threads that block, and no locks held across a wait. A Flow is a
set of Steps that read and write Attributes, publish and consume Channel
messages, and wait on Timers. So you may wonder whether some concurrent logic
cannot be written as a Flow.
The proof shows that any concurrent logic you can write with the constructs
above can also be written as a Flow.
The translation is a construction for the proof, not a compiler that Dex
ships. It uses about one Step for each statement, which is not how to model
an application. Model your own Flow with the
[design patterns](https://docs.superdurable.io/design-patterns.md).
## How each construct is built
| Construct | Dex building blocks | Related design pattern |
| ------------------ | -------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | -------------------------------------------------------------------------------------- |
| Thread | A chain of Steps, usually one for each statement. **wait** takes three Steps, and **sleep** and timed **select** add an entry Step. The thread's position and local state travel in the Step input. A running thread is one active Step execution at a time. | |
| **fork** | **GoToMany** to the parent's next Step and the child's first Step. | |
| **join** | The ending thread publishes one message to its join Channel, then returns **DeadEnd**. The joining Step waits with **AnyOf** on that Channel and on its own cancel Channel. | [Await Parallel Steps](https://docs.superdurable.io/design-patterns/parallel/await.md) |
| Mutex | A Channel that holds one token while the mutex is free. **lock** waits for the token with **ForOne**. Waiters are served in the order they started waiting. **unlock** publishes the token back. | [Critical Section](https://docs.superdurable.io/design-patterns/critical-section.md) |
| Condition variable | An Attribute holds the list of waiting threads. Each waiter has its own Channel. **wait** adds the thread to the list, releases the mutex, waits on its Channel, then takes the mutex again. **signal** removes the first waiter and publishes to its Channel. **broadcast** does this for every waiter. | |
| **sleep** | One timed Step. Its **WaitFor** returns **AnyOf** with a Timer and the thread's cancel Channel. | |
| Timed **select** | The same timed Step. It waits with **AnyOf** on a Timer, the input Channel, and the cancel Channel. Only the winning Condition consumes a message. | [Deferred Choice](https://docs.superdurable.io/design-patterns/deferred-choice.md) |
| Cancellation | A message on the canceled thread's cancel Channel. The thread sees it only at a point where it would block. | |
| Exception | The handler stack travels in the Step input. **throw** is a **GoTo** to the handler's Step. | |
| Exit or failure | **ForceComplete** with the result, or **ForceFail** with the error. | |
| External effect | An **Execute** whose only effect is that external call. | |
An Attribute lock would not work for the mutex, because it covers one Step
method and not a wait. A Channel token can be held
across many Steps and waits.
## How it was checked
The proof is written in the Lean proof assistant, which checks every step.
## Failures
This proof covers runs without failures. The
[Failure transparency proof](https://docs.superdurable.io/correctness-and-expressiveness/failure-transparency-proof.md)
extends it to crashes, recovery, retries, and redelivery. Under the conditions
on that page, removing the repeated external effects from a run with failures
leaves a run without failures. Combined, the two proofs show that a
well-formed program of the language runs on Dex with the events of a run
without failures, except that external effects can repeat.
## Related evidence
The [Workflow Patterns evaluation](https://docs.superdurable.io/correctness-and-expressiveness/workflow-patterns.md)
rates Dex against 43 workflow patterns, each with a runnable example and a
test against a real server. The patterns test the real server on common
cases. The proof covers every program of the language.