Skip to content

docs: AFFIRMATION.adoc overclaims 'zero escape hatches'; proof-debt.md cites a nonexistent script and CI job #831

Description

@hyperpolymath

Split out of #696, whose two substantive halves are now closed (the Idris2
duplication by #815, the Zig CI gate by the #812/#813/#696 PR). Its "For
contrast" section recorded two documentation defects that are not part of
either fix, and they should not be closed silently along with them.

1. AFFIRMATION.adoc overclaims

It states zero escape hatches. Measured across 22 .idr files: 0
assert_total, 0 postulate, 0 %hint, and 8 believe_me — 4 in comments
carrying an explicit -- hypatia: allow pragma, 4 in a deliberate scanner
fixture. None execute, so the spirit of the claim holds, but the literal claim
is false as written.

Acceptance criteria

  • The claim is scoped to be exactly true — e.g. "zero escape hatches
    outside test/soundness/fixtures/" — rather than deleted or left
    absolute.
  • The scoping names the fixture directory explicitly, so a future
    believe_me added outside it still contradicts the document.
  • The counts quoted are re-measured at the time of the fix, not copied
    from this issue.

2. docs/proof-debt.md cites things that do not exist

  • It instructs readers to run scripts/check-trusted-base.sh. No such
    script exists.
    Either add it or remove the instruction.
  • It claims a check-trusted-base CI job enforces annotation. No such
    job exists
    in any workflow. Either add it or remove the claim.
  • Its headline count is derived from "agent worktrees under
    .claude/worktrees/", a directory that no longer exists. Re-derive the
    count from the live tree, and state what it was derived from.
  • A reader following the document end to end hits no missing file or job.

Evidence: docs/DEBT-REGISTER.md (P-1, P-2, P-3, C-4).

Note on framing: a document that instructs readers to run a nonexistent
verification script is worse than one that says nothing, because it reads as
evidence that checking happens. That is the reason to fix it rather than to
file it as cosmetic.

Activity

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    documentationDocs, prose, diagrams, READMEs, ADRsproofsFormal verification: Agda, Coq, Idris, Lean, Z3/SMT, axiom debt

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions