Cure v0.12.0: A Dependently-Typed Language for the BEAM

The BEAM virtual machine has Erlang. It has Elixir. It has Gleam and LFE and Caramel and half a dozen others. What it has never had is a language that proves your code correct at compile time using an SMT solver.

Until now.

What is Cure?

Cure is a programming language that compiles to BEAM bytecode. It runs on the same VM as your Erlang and Elixir code – same OTP, same supervision trees, same hot code loading. But it adds something those languages deliberately left out: a type system that can reason about values, not just shapes.

type NonZero = {x: Int | x != 0}

fn safe_divide(a: Int, b: NonZero) -> Int = a / b

That NonZero is a refinement type. The constraint x != 0 is not a runtime check. It is a theorem. The compiler sends it to Z3, an SMT solver, and Z3 proves (or disproves) it at compile time. If you try to call safe_divide(10, 0), the compiler catches it before a single BEAM instruction executes.

Why the BEAM?

The BEAM is the best runtime in existence for concurrent, fault-tolerant systems. OTP supervisors, hot code upgrades, distribution – nothing else comes close. But its dynamically-typed nature means entire classes of bugs survive until production. Dialyzer helps, but it’s a success typings tool, not a proof system.

Cure keeps everything the BEAM gives you and adds compile-time guarantees on top. A Cure module compiles to a regular .beam file. You can call it from Erlang or Elixir. You can call Erlang or Elixir from Cure:

@extern(:erlang, :abs, 1)
fn abs(x: Int) -> Int

The Syntax

Cure uses indentation structure. No do/end, no braces, no closing delimiters. The visual layout is the structure:

mod MyApp.Math
  fn factorial(n: Int) -> Int
    | 0 -> 1
    | n -> n * factorial(n - 1)

  fn classify(x: Int) -> String
    | x when x > 0 -> "positive"
    | x when x < 0 -> "negative"
    | _             -> "zero"

Multi-clause functions use | for pattern dispatch. Guards use when. Everything is an expression – the last expression in a block is its value.

First-Class Finite State Machines

This is where Cure gets interesting for anyone building protocols, workflows, or embedded systems. FSMs are a language construct:

fsm TrafficLight
  Red    --timer-->     Green
  Green  --timer-->     Yellow
  Yellow --timer-->     Red
  *      --emergency--> Red

That is a complete, compilable file. The compiler generates an OTP gen_statem module with start_link, send_event, and get_state. But before it generates anything, it verifies:

• Reachability: every state is reachable from the initial state.
• Deadlock freedom: every non-terminal state has at least one outgoing transition.
• Terminal validity: declared terminal states exist in the transition graph.

Protocols That Compile to Fast Dispatch

Cure’s protocol system compiles to multi-clause guard-dispatched functions. There is no runtime dictionary lookup, no vtable indirection:

proto Show(T)
  fn show(x: T) -> String

impl Show for Int
  fn show(x: Int) -> String = Std.String.from_int(x)

impl Show for Bool
  fn show(x: Bool) -> String = if x then "true" else "false"

The Numbers

569 tests. Zero credo issues in strict mode. Zero compilation warnings. 44 Elixir source files implementing the compiler, type system, SMT integration, optimizer, FSM runtime, LSP, MCP, and CLI. 12 stdlib modules written in Cure itself. 10 example programs. 4 documentation guides.

Getting Started

git clone https://github.com/am-kantox/cure.git
cd cure
mix deps.get
mix test
mix escript.build
./cure run examples/recursion.cure

The repository is at github.com/am-kantox/cure.