G001
Do algebraic design docs improve coding agents' quality, token use, or time against no supplied docs and prose docs?
Hypothesis: Describing a codebase algebraically instead of semantically reduces inference via proofs which reuse repeated reasoning.
- E009-E010Generation · fresh codebase · 1 imperative stageOne-stage build: algebraic docs missed the preset quality marginOne build stage, two builder models. Algebraic docs scored below no docs with one model and above with the other, both times by less than the rule's threshold.
- E015-E017Generation · fresh codebase · 5 imperative stagesFive-stage builds: algebraic docs missed the quality margin and used more tokensTwo runs, two builder models. The algebraic arm never beat no docs by the rule's threshold and used the most build tokens in both runs.
- E018-E025Generation · fresh codebase · 5 imperative stages · z3-checked algebraFive-stage z3 builds: quality margin unmet; tokens fell in both runsTwo repeat runs. The algebra arm proved its design with z3 before coding. Its score stayed close to no docs, and it used fewer build tokens in both runs.
- E020-E026Generation · fresh codebase · 7 declarative stages · z3-checked algebraSeven declarative stages: quality margin unmet; tokens rose in three runsThree repeat runs with declarative prompts. The z3-checked algebra arm scored level with or below no docs and used more build tokens in every run.
- E022-E023Retrieval · 400k-line codebase · 5 questions · z3-checked algebraDesign docs missed quality and efficiency targets in retrievalTwo builder models answered five questions each. Neither design form met the retrospective +0.1 correctness target and saved tokens and time in both runs.
- E024Generation · 400k-line codebase · 5 imperative stages · z3-checked algebraExisting-codebase changes: z3 algebra missed the quality margin and used more tokensThree repeat runs extending an application its design records already describe. No doc form beat no docs by the rule's threshold, and the algebra arm used more build tokens in every run.