Cure Programming Language

Dependent Types. SMT Verification. Native FSMs. On the BEAM.

A strongly-typed, dependently-typed programming language that brings mathematical correctness guarantees to the battle-tested BEAM virtual machine. Build systems where verification matters more than convenience.

Core Features

What makes Cure unique in the BEAM ecosystem

🎯

Dependent Types

Express and verify invariants at compile time with length-indexed vectors, refinement types, and SMT-backed constraint solving.

🎆

First-Class FSMs

State machines as native syntax with arrow-based transitions. The compiler verifies reachability, deadlock freedom, and invariant preservation.

🔬

SMT Verification

Z3 and CVC5 solver integration validates your types and state machines. Your types are theorems, proven before execution.

✅

Exhaustive Patterns

No if-then-else. Pattern matching with guards ensures every case is handled. The compiler proves completeness.

⚡

Type Optimizations

Monomorphization, specialization, and inlining provide 25-60% performance improvements over baseline.

🏗️

BEAM Integration

Compiles to BEAM bytecode with full OTP compatibility. Interoperate with Erlang and Elixir ecosystems seamlessly.

🔌

LSP Support

Complete Language Server Protocol implementation with real-time diagnostics, hover info, and IDE integration.

📚

Standard Library

12 working modules including core, io, list, fsm, result, vector, string, math, and more with verified runtime execution.

Why Cure?

A principled language that focuses on what’s missing, not what’s already there

🎯 Dependent Types with SMT

Express and verify invariants at compile time. Vector operations that can’t fail. Array access that’s proven safe.

🎆 Native FSM Syntax

State machines aren’t a pattern—they’re native syntax with compile-time safety verification by SMT solvers.

🚫 No If-Then-Else

Forces you to think in pattern matching and exhaustive cases. No forgotten edge cases. Every decision point is explicit.

🔒 Verification > Convenience

When correctness matters more than convenience. For safety-critical systems, financial transactions, industrial control.

🤝 BEAM Interoperability

OTP fault tolerance, hot code reloading, distributed computing, and full Erlang/Elixir ecosystem access.

📈 Production Ready

Complete compiler pipeline, comprehensive testing, working standard library, and LSP support for modern development.

# The type system proves this is safe—no runtime checks needed
def safe_head(v: Vector(T, n)): T when n > 0 =
head(v)

# FSMs with native syntax and compile-time verification
fsm TrafficLight do
Red --> |timer| Green
Green --> |timer| Yellow
Yellow --> |timer| Red
Green --> |emergency| Red
end

# Exhaustive pattern matching—compiler proves all cases handled
def classify(x: Int): Atom =
match x do
n when n < 0 -> :negative
0 -> :zero
n when n > 0 -> :positive
end

When to Use Cure

✅ Perfect For

• Safety-critical finite state machines
• Systems with complex invariants
• Domains where correctness > convenience
• Trading systems, industrial control
• Medical devices, aerospace applications

❌ Not Ideal For

• Rapid prototyping (use Elixir)
• Scripts and glue code
• General web development (Phoenix is excellent)
• When you need maximum ecosystem libraries

Quick Start

# Build the compiler
make all

# Try an example
./cure examples/06_fsm_traffic_light.cure

# Run the compiled program
erl -pa _build/ebin -noshell -eval "'TrafficLightDemo':main(), init:stop()."

# Run tests
make test