Cure v0.7.0 - Dependently-Typed Programming for the BEAM

Features

• Dependent types with refinement constraints for compile-time verification
• First-class finite state machines with native syntax and transition verification
• SMT solver integration (Z3, CVC5) for automated theorem proving
• Exhaustive pattern matching enforced by the compiler
• Type-directed optimizations (monomorphization, specialization, inlining)
• Full BEAM bytecode compilation with OTP compatibility
• Language Server Protocol (LSP) implementation for IDE integration
• Complete standard library with 12+ modules
• Typeclass system with automatic derivation

Why Cure

• Mathematical correctness guarantees through dependent types and SMT verification
• Native FSM syntax eliminates boilerplate and enables compile-time safety analysis
• Runs on the battle-tested BEAM VM with OTP fault tolerance and distribution
• Designed for safety-critical systems where verification matters more than convenience
• Full interoperability with Erlang and Elixir ecosystems
• Production-ready toolchain with compiler, LSP server, and comprehensive testing

Quick Start

# Build the compiler
make all

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

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

# Run tests
make test

Example Code

# Dependent types prove safety at compile time
def safe_head(v: Vector(T, n)): T when n > 0 =
  head(v)

# Native FSM syntax with verified transitions
fsm TrafficLight do
  Red --> |timer| Green
  Green --> |timer| Yellow  
  Yellow --> |timer| Red
  Green --> |emergency| Red
end

# Refinement types constrain values
def safe_divide(a: Int, b: {x: Int | x != 0}): Int =
  a / b

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

See More Examples