Cure

Cure

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

Current release: v0.23.0 -- Packaging, Proof, and Polish. Remote package registry with Ed25519-signed publishes and a Rekor-style transparency log, Std.Json and Std.Http in stdlib, property-based shrinking, cure doctor / cure fix / cure test --cover, a :telemetry bridge, and the cure_brainloop showcase example. 

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.

Getting Started

Install, compile, and run your first Cure program.

Language Guide

Syntax, keywords, operators, and all language constructs.

Type System

Bidirectional checking, refinement types, SMT verification.

Finite State Machines

First-class FSMs with compile-time structural verification.

Standard Library

27 self-hosted modules, ~290 functions.

Pattern Matching

Every pattern shape: literals, lists, tuples, maps, records, ADTs, bitstrings, pins, guards, and nested destructuring.

Roadmap

What shipped through v0.23.0 and what comes next.