These primary sources informed the design discussion. They are foundations and comparisons to study, not evidence that the proposed combination has already been implemented or proved sound. The language specifications define their own proposed behavior.
| Source | Relevant topic |
|---|---|
| F star proof oriented programming | Dependent and refinement types, effects, proof automation |
| Flux liquid types for Rust | Refinements working with ownership |
| Verus modes | Distinguishing specification, proof, and executable code |
| Koka language documentation | Effect inference and effect-polymorphic programming |
| Sound gradual verification with symbolic execution | Sound interaction of partial specifications and runtime checks |
| Idris 2 quantitative type theory in practice | Dependent types, erasure, and usage information |
| GHC rewrite rules | User rewrite interfaces, matching, phases, and trust |
| Stream fusion from lists to streams to nothing at all | Producer state machines and elimination of intermediates |
| Formalization of stream fusion | Formal stream equivalence and fusion reasoning |
| Agda coinduction | Guarded corecursion and stream bisimulation |
| Lamport on safety liveness and fairness | Infinite behaviors and temporal properties |
| PlusCal tutorial on liveness | Progress and fairness assumptions |
| LLVM language reference | Vector IR, data layout, masked memory operations, and backend semantics |
| Alive2 bounded translation validation | Checking compiler transformations and limits of bounded validation |
FFI, WebAssembly and concurrency sources
Standards context checked 22 October 2026. Runtime support must still be checked for the selected deployment host; a standards release does not imply every host implements it.
| Source | Relevant topic |
|---|---|
| Rustonomicon FFI | Native ABI, callbacks, ownership and unwinding concerns |
| WASI 0.3 release | Released 11 June 2026; async functions, futures and streams |
| WIT reference | Worlds, interface types and owned/borrowed resources |
| Component model concurrency design | Tasks, async calls and component concurrency semantics |
| WebAssembly security | Sandbox and host security boundaries |
The proposed structured-concurrency, STM and foreign-proof policies in this draft are language-design choices. These references do not establish their soundness.
Further research required
The integration of dependent staging, typed module identity, dynamic software updating, and ownership-preserving migration needs a dedicated literature review before the core is finalized. This draft intentionally treats its mechanisms for those features as design proposals. It does not claim novelty or a proven advantage over every existing system.
Runtime and effect inspirations
-
Zig 0.16 release notes: I/O as an interface — explicit implementation passing for I/O.
-
Koka language book — effect polymorphism and handler-based control abstractions.
The lexical capability and sequencing module combination in this draft is our proposal; these sources do not prove its integration sound.