Cure

Dependently-typed programming language for the BEAM virtual machine with first-class finite state machines and SMT-backed verification.

Current release: v0.25.0 -- Typed Supervision Trees. The Melquiades Operator <-| (unicode alias ✉) for typed sends, an actor container that compiles to a loaded GenServer module, a sup container that compiles to a verified Supervisor behaviour module with compile-time structural checks, and a new stdlib surface (Std.Actor, Std.Process, Std.Supervisor) exposing the runtime from Cure source. See the new Actors reference for the tour.

mod MyApp.Math
  use Std.{Result, Option}

  type Sign = Positive | Negative | Zero
  type NonZero = {x: Int | x != 0}

  fn factorial(n: Nat) -> Nat
    | 0 -> 1
    | n -> n * factorial(n - 1)

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

  fn classify(x: Int) -> Sign
    | x when x > 0 -> Positive
    | x when x < 0 -> Negative
    | _             -> Zero

Cure compiles .cure source files to BEAM bytecode. Your Cure modules run natively on the Erlang VM alongside Erlang and Elixir code -- same OTP, same supervision trees, same hot code loading.

The type system is bidirectional, with refinement types verified at compile time by Z3. The constraint x != 0 in NonZero is not a runtime check -- it is a theorem the compiler proves before a single BEAM instruction executes.

Finite state machines are a first-class language construct. They compile to OTP gen_statem modules with compile-time verification of reachability and deadlock freedom.

v0.25.0 extends the process-oriented surface with typed actor containers that compile to loaded GenServer modules and sup containers that compile to verified Supervisor behaviour modules, wired together by the Melquiades Operator <-|.

Cure

Getting Started

Language Guide

Type System

Finite State Machines

Actors

Standard Library

Pattern Matching

REPL

Roadmap