Cure

Verification-First Programming

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 fully compiled modules: core, io, list, fsm, result, pair, vector, string, math, system, rec, and typeclasses with 100+ functions.

Documentation

31+ comprehensive guides covering language features, APIs, FSMs, typeclasses, SMT integration, and more.

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