This file backs every factual claim in README.adoc with code paths and honest caveats. Read it if you are doing due diligence on whether the story matches the code.
Dependent types, linear types, session types, QTT, effect systems, modal types, proof-carrying code.
- How this is implemented
-
The Idris 2 formal specifications in
src/abi/define the type system interfaces and soundness properties. The Rust kernel insrc/kernel/implements the bidirectional type checker, proof engine, effect tracker, and session protocol manager. - Caveat
-
Phase 0 status. The Idris 2 specs define the target type system. The Rust kernel implementation is under active development. Coverage is by design, not by current achievement.
Dependent types prove type system soundness. Zero believe_me.
- How this is implemented
-
src/abi/contains Idris 2 modules specifying the type system. Thebelieve_mecount is verified by CI (grep forbelieve_meinsrc/abi/). - Caveat
-
The specs prove soundness of the type system definition. They do not prove soundness of the Rust implementation. Alignment between spec and implementation is a manual obligation, mitigated by the FFI bridge and generated C headers.
_Typell is to PanLL what LLVM is to Clang: the compiler infrastructure that any frontend can consume._
- How this is implemented
-
Typell exposes a JSON-RPC verification protocol (
src/kernel/protocol/). PanLL, VS Code extensions, CLI tools, and CI/CD pipelines all consume Typell through this protocol. - Caveat
-
The LLVM analogy is architectural, not operational. LLVM has hundreds of production frontends and backends. Typell has one primary consumer (PanLL) under development. The analogy describes the design intent, not the current ecosystem.
_VCL-dt (VeriSimDB), GQL-dt (LithoGlyph), KRL-dt++ (QuandleDB)_
- How this is implemented
-
Backend directories exist in
src/backends/. VCL-dt is a port from ReScript. GPNL-dt bridges to Lean 4. KRL-dt++ is designed from scratch. - Caveat
-
These backends are in design/early implementation phase. None are production-ready. The strategies described (8-modality queries, RATIONALE clause, equality saturation) are the target features, not currently shipping capabilities.
_Zig (ffi/zig/): C ABI compatibility per hyperpolymath universal standard._
- How this is implemented
-
ffi/zig/contains the Zig FFI layer. Auto-generated C headers live ingenerated/abi/. The hyperpolymath universal standard is documented indocs/design/ABI-FFI-README.md. - Caveat
-
The FFI bridge is the soundness-critical layer. If the Zig FFI misrepresents the Idris 2 spec’s types to the Rust kernel, soundness is lost. Integration testing across this boundary is essential and ongoing.
|
Caution
|
Phase 0: Implementation is beginning. The architecture, specs, and directory structure exist. The running type checker, proof engine, and backends are under active development. |
|
Caution
|
Spec-implementation alignment is not machine-checked. Soundness of the Rust kernel against the Idris 2 specs is a manual obligation. No extraction or certified translation tool exists yet. |
|
Caution
|
Backend implementations are early. VCL-dt, GPNL-dt, and KRL-dt++ are in design/initial implementation. None handle production query workloads. |
|
Caution
|
Echidna delegation boundary is underspecified. Typell delegates complex proofs to Echidna. The boundary between what Typell proves internally and what it delegates is not yet formally delimited. |
| Path | Proves / Defines |
|---|---|
|
Idris 2 formal specs for type system soundness |
|
Bidirectional type checker (Rust, under development) |
|
Proof engine (Rust, under development) |
|
Session protocol manager (Rust, under development) |
|
Full design vision document |
|
ABI/FFI standard documentation |
abc def ghi jkl mno pqr stu