Cure language
Build dependable systems on the BEAM with dependent types
Cure sends every program through one dependent compiler pipeline: elaboration, kernel checking, quantitative erasure, and native BEAM code. Indexed types and ordinary OTP concurrency live in the same language.
mod Counter
type State = State(Nat)
fn next(State(n)) -> State =
State(n + 1)
fn value(State(n)) -> Nat = nMake invariants explicit
Express relationships between values in indexed types and prove them with evidence independently checked by the dependent kernel.
Model concurrency directly
Actors, supervisors, applications, and finite-state machines fit the language instead of being hidden behind an untyped boundary.
Stay native to the BEAM
Compile to BEAM bytecode, use OTP, and work alongside Erlang and Elixir without giving up Cure’s checks.
A clear path
From idea to running system.
Cure is designed around the way BEAM systems are built: describe the state, make the messages precise, and let supervision handle failure.
01
Describe the domain
Use algebraic and indexed data types, dependent functions, and pattern refinement to give values meaningful, machine-checked structure.
02
Connect the pieces
Build actors and state machines with typed transitions and messages that make invalid states difficult to represent.
03
Run with confidence
Compile to the BEAM and deploy with the fault-tolerance and tooling your production system already depends on.
Choose your next step.
Learn the language, explore OTP concurrency, or inspect the standard library.