|
- A statically typed quantum programming language with Rust-like syntax and conservative quantum extensions that preserve the look and feel of Rust.
- Linear qubit ownership and mutable borrowing: no-cloning and qubit-use discipline are enforced statically by the type checker.
- Safe ancilla management, with support for automatic uncomputation.
- Lightweight quantum contracts for tracking properties of entanglement for program qubits at compile time.
- Designed for formal verification, with program properties proved in Lean 4 against a type-safe intermediate representation.
- Detailed diagnostics designed for both human developers and AI-assisted code generation.
- Practical by construction: compiles to OpenQASM 3, with QIR support planned.
- Built for the fault-tolerant quantum computing era.
Code example:
general fn coin_flip() -> bit {
let q = qalloc();
H(&q);
measr(q)
}
general fn main() -> bit {
coin_flip()
}
| Capability | Status |
|---|---|
| Language Design & Docs | Implemented |
| Lexer | Implemented |
| Parser | In progress |
| Surface AST | In progress |
| Semantic Analyzer | In progress |
| De-sugaring & Canonical AST | Planned |
| Scope & Name Resolution | Planned |
| Type Checker & Typed AST | Planned |
| Quantum Lambda Calculus IR | Planned |
| Lambda Calculus Code Generator | Planned |
| Idris2 DSL | Implemented |
| Idris DSL Lowering Pass | Planned |
| OpenQASM 3 Serializer | In progress |
| Alpha release | Fall 2026 |
| Lean Interface | Planned |