Cure

Cure

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

Current release: v0.27.0 -- Applications and Releases. An app container wraps an entire supervision tree into a first-class OTP application declared in Cure source; the same compiler cycle emits the <name>.app OTP resource file and a loaded Application-behaviour module, and the new cure release subcommand packages the whole thing as a bootable BEAM release. See the new Applications reference for the tour, or the Actors reference for the typed supervision primitives underneath. 

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 <-|.

v0.26.0 wraps the supervision tree into a first-class OTP application: an app container compiles to an Application callback module, emits an OTP <name>.app resource file, and is packaged by cure release as a bootable BEAM release.

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.

Actors

Typed supervision trees with the Melquiades Operator <-|, actor and sup containers, and stdlib wrappers for links, monitors, and trap_exit.

Applications

First-class OTP applications and BEAM releases: the app container, Cure.toml [application] and [release] sections, and the cure release subcommand.

Standard Library

30 self-hosted modules, ~320 functions.

Pattern Matching

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

REPL

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

Roadmap

What shipped through v0.27.0 and what comes next.