Cure
Dependently-typed programming language for the BEAM virtual machine with first-class finite state machines and SMT-backed verification.
Current release: v0.18.0 -- Sigma & Pi types, propositional equality, implicit arguments, holes, totality, path-sensitive refinement, records, REPL, watch mode.
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.
Dependent Types new
Sigma, Pi, equality types; implicit arguments, holes, totality.
Roadmap
What shipped through v0.18.0 and what comes next.