Cure

Cure

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

Current release: v0.24.1 -- The REPL You Deserve. A full rewrite of cure repl on top of a raw-mode line editor with live Makeup-powered syntax highlighting, persistent history, Ctrl+R incremental reverse search, Tab completion, a minimal vi mode, and a Marcli-rendered :help. See the new REPL reference for the full key-bindings table and meta-command list. 

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.

REPL

The v0.24.0 raw-mode REPL: live syntax highlighting, persistent history, reverse search, Tab completion, and a minimal vi mode.

Roadmap

What shipped through v0.24.1 and what comes next.