Cure

is a dependently typed programming language built specifically for the BEAM (Erlang VM), combining indexed types, kernel-checked proofs, first-class finite state machines, and native OTP actor concurrency in a single unified compiler pipeline.

The Pitch

Building mission-critical distributed applications on the BEAM demands exceptional fault tolerance and state consistency. While OTP processes and GenServers handle runtime resilience gracefully, complex domain invariants — such as protocol state sequences, non-empty list guarantees, and matrix dimensions — traditionally fall back to dynamic runtime checks.

Cure solves this by bringing dependent type checking directly to the Erlang ecosystem. Programs pass through an elaboration pipeline, kernel verification, and quantitative type erasure to produce clean, native BEAM bytecode. Indexed types allow you to encode domain rules directly into function signatures, while built-in SMT solver integration (via Z3) automates proof resolution without sacrificing developer velocity.

Why Cure?

Dependently Typed Kernel

Express precise invariants using indexed data types and dependent functions. Function signatures state what values mean, while a minimal, trusted type-checker kernel verifies compliance before codegen.

First-Class Finite State Machines

FSMs are not secondary libraries or wrapper modules in Cure — they are first-class language constructs. Transition rules, valid message sequences, and state payloads are checked at compile time, eliminating invalid state representation entirely.

OTP & BEAM Native

Cure compiles directly to BEAM bytecode. Actors, supervision trees, and message-passing primitives fit naturally into the language syntax, allowing Cure modules to seamlessly interoperate with existing Erlang and Elixir applications.

Modern Developer Tooling

Cure ships with an active developer environment out of the box:

• Full LSP Server ( Cure.LSP.Server ): Inlay hints, signature help, code lenses, semantic tokens, and source-preserving formatting.
• Interactive REPL ( cure repl ): Multi-line evaluation, meta-commands ( :t , :doc , :effects , :holes ), and persistent history.
• Watch & Test Harness : Built-in test execution with doctest support ( cure test --doctests ) and sub-200ms file watching.

The Tech

Bottom Line

Cure proves that dependent types and fault-tolerant actor systems belong together. By checking invariants at compile time and erasing proof overhead before generating BEAM bytecode, Cure lets you write self-documenting, provably correct software on the platform built for reliability.