---
title: "Correctness and expressiveness"
description: "This section answers two questions about Dex."
canonical_url: "https://docs.superdurable.io/correctness-and-expressiveness/"
source: "docs/content/correctness-and-expressiveness/index.mdx"
locale: "en"
---

# Correctness and expressiveness

This section answers two questions about Dex.

- **Expressiveness**: can Dex express the programs you need?
- **Correctness**: does Dex stay correct when processes, machines, or networks
  fail?

## Expressiveness

The [Expressiveness proof](https://docs.superdurable.io/correctness-and-expressiveness/expressiveness-proof.md)
shows that any program in a small concurrent language, with threads, locks,
timers, and cancellation, can be written as a Dex Flow that behaves the same.
A computer checks every step of the proof. The
[paper](https://docs.superdurable.io/papers/dex-expressiveness.pdf) has the full argument.

The [Workflow Patterns evaluation](https://docs.superdurable.io/correctness-and-expressiveness/workflow-patterns.md)
rates Dex against the 43 control-flow Workflow Patterns. Researchers use these
patterns to compare workflow languages and engines. Each rating comes with a
runnable example and an integration test.

## Correctness

The [Step guarantees](https://docs.superdurable.io/concepts/step.md#guarantees) state what Dex promises when
a Step method fails or runs again.

The [Failure transparency proof](https://docs.superdurable.io/correctness-and-expressiveness/failure-transparency-proof.md)
covers server crashes, standby takeovers, retries, Workers that keep running
after Dex gave up on them, and duplicate results. These failures add only
repeated external effects: remove them, and the rest is a sequence the Flow
can produce without failures. For fair runs, the ending stays the same too.
The proof's page lists its conditions, such as **SYNC** methods only and
retries that never run out. This proof is also computer-checked, and the same
[paper](https://docs.superdurable.io/papers/dex-expressiveness.pdf) has the full argument.

Combined, the two proofs cover every well-formed program of the small
concurrent language. On Dex, such a program produces the events of a run
without failures, except that external effects can repeat, and a repeat can
come late.
[What this means for your code](https://docs.superdurable.io/correctness-and-expressiveness/failure-transparency-proof.md#what-it-means-for-you)
says how to make repeats safe.