Cure
Verification-First Programming
Verification-First Programming
Comprehensive code samples demonstrating Cure language features, from basic list operations to advanced finite state machines and dependent types.
Fundamental list processing with map, filter, and fold operations
Length-indexed vectors with compile-time size verification
Safe error handling with Result type and combinators
Handling optional values without null references
Pattern matching with guard clauses for precise control flow
Guard constraints in function signatures
Recursive function definitions and patterns
Advanced guard patterns and combinations
Classic traffic light FSM with timer and emergency transitions
Enhanced traffic light with state payload tracking
Compile-time verification of FSM properties and invariants
Refinement constraints for non-zero divisors, positive numbers, and bounded values
Typeclass system with Show, Eq, and custom instances
Automatic typeclass derivation for records
Complex refinement constraints and dependent type patterns
SMT-backed verification of refinement type constraints
Polymorphic algorithms with typeclass constraints
Functor, Monad, and higher-kinded type patterns
Implementing and using the Show typeclass
Function composition with the pipe operator
Record types with pattern matching and updates
Anonymous functions and closures
Pattern matching on tuples and nested structures