Erlang Meets Idris: Cure Programming Language
17 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 features like SMT-backed constraint solving.
- Native syntax for state machines with compile-time verification of reachability and deadlock freedom.
- Integration with Z3 and CVC5 solvers to validate types and state machines.
- Pattern matching with guards ensures exhaustive case handling, proven by the compiler.
- Performance improvements of 25-60% over baseline due to monomorphization and inlining.
- Full compatibility with BEAM bytecode and seamless interoperability with Erlang and Elixir ecosystems.
- Includes a 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 features include safe vector operations, native FSM syntax, and exhaustive pattern matching.