Cure – Verification-First Programming for the Beam
20 days ago
- #verification
- #BEAM
- #programming-language
- Cure is a strongly-typed, dependently-typed programming language for the BEAM virtual machine.
- It offers mathematical correctness guarantees and verification at compile time.
- Features include length-indexed vectors, refinement types, and SMT-backed constraint solving.
- Native syntax for state machines with compiler-verified reachability and deadlock freedom.
- Integration with Z3 and CVC5 solvers to validate types and state machines.
- Pattern matching with guards ensures all cases are handled, eliminating forgotten edge cases.
- Performance improvements of 25-60% over baseline due to monomorphization and inlining.
- Full OTP compatibility and seamless interoperability with Erlang and Elixir ecosystems.
- Complete Language Server Protocol implementation for IDE integration.
- 12 fully compiled standard library modules with over 100 functions.
- 31+ comprehensive guides covering language features, APIs, and SMT integration.
- Designed for safety-critical systems, financial transactions, and industrial control.
- Example code snippets demonstrate safe vector operations, FSM syntax, and exhaustive pattern matching.