GoKawiilZIL Lean
ZIL is a small relational language for describing named objects, the relationships between them, and rules that derive additional relationships.
A relation has three parts:
subject ── relation ──▶ object
For example:
lean.Parser.parse ── implements ──▶ requirement.parseInput
ZIL Lean implements this model inside Lean 4. Lean checks definitions, executable programs, theorem statements, and proofs. ZIL records how those checked declarations relate to requirements, documents, tests, tasks, dependencies, and other parts of a project.
The same project map can answer questions such as:
which declaration implements this requirement? which theorem validates this component? which modules depend on this declaration? which task is waiting for this result? which declarations should be reviewed after this change?
Developers, review tools, CI, documentation tools, and AI assistants can query the same stored relationships.
... continue reading