Cure – Verification-First Programming for the Beam

3 days ago 2

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