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.

Get Started Read the Docs

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

# 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