Cure

Cure

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

Current release: v0.20.1 -- The Shape of Things. Plain # comments as first-class AST nodes, full Elixir-style bitstring segments (<<x::utf8, rest::binary>>), a Wadler-style algebra pretty-printer behind cure fmt --algebra, and structural refinement narrowing via Cure.Types.PatternRefinement. 

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

18 self-hosted modules, ~200 functions.

Pattern Matching

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

Roadmap

What shipped through v0.20.1 and what comes next.