Skip to content

Evidence: define the three evidence kinds and their formats #6

Description

@hyperpolymath

Charter artefact (2) explicit evidence. Sketch area: src/evidence/ (src/evidence/README.adoc).

Define the witness behind every claim. No envelope without evidence.

Scope

  • The three kinds: proof (Coq/Agda/Idris2), check (decision-procedure result), runtime discipline (declared, enforced invariant).
  • On-disk/in-memory representation of each kind.
  • The link from a Core checking result to the evidence it produced.
  • Validation that an envelope's cited evidence actually supports its claim.

Done when

  • A spec/format for each evidence kind exists.
  • The manifest emitter can refuse an envelope whose evidence is missing/insufficient.
  • Evidence kind is recorded honestly (a check is never labelled a proof).

Ref: docs/architecture/DESIGN-DISCIPLINE.adoc, docs/status/PROOF-NEEDS.adoc.

Metadata

Metadata

Assignees

No one assigned

    Labels

    designDesign of an interface, protocol, grammar, or type theoryenhancementNew capability or improvement to existing behaviour

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions