Skip to content

AFFIRMATION.adoc

Latest commit

 

History

History
73 lines (59 loc) · 2.98 KB

AFFIRMATION.adoc

File metadata and controls

73 lines (59 loc) · 2.98 KB
Raw

AFFIRMATION — anytype, as of <UTC timestamp at signing>

the No-Bullshit file: what we affirm was true and checkable at this moment.

Table of Contents

What this is

A short, dated, signed snapshot of what can be honestly and verifiably claimed about anytype — the reference kernel for Equality Theory — at one exact commit. The README is the vision; EXPLAINME.adoc is the mechanism; this file is the receipt. It is our best honest belief at a stamped instant, binding on our honesty, not a claim of infallibility.

Note

The anchor below carries <…> fields (commit SHA, timestamp, toolchain) that are filled in at signing time, in the same session that runs the checks. Until then this file is a draft.

What we affirm

Claim Status Evidence

The repository is RSR-shaped and validates

affirmed-pending-run

just validate at the anchor SHA

The kernel’s design is written down (pluggable L2 grades; L1 conversion; gates)

affirmed

README.adoc, EXPLAINME.adoc

anytype is the implementation; systemet is the theory it pins upstream

affirmed

.machine_readable/6a2/anchors/ANCHOR.a2ml, ECOSYSTEM.a2ml

What we do NOT claim

  • The kernel is an MVP cut, not a general-purpose type checker. No dependent types, no branching, no L3 recursion, no L0 lowering, no L4 effects.

  • No soundness proof for the checker. The grade-algebra laws are machine-checked proof fields and the golden matrix is real, but progress/preservation for the L1 checker is not proven.

  • The totality gate is syntactic (no recursion constructor in the type-index language), not a termination analysis.

  • TEA-erasure is OPEN (in systemet) and not started here. Do not cite it.

  • The seam transport is a spawned process, not in-process linkage; five never-compiling template proof modules are quarantined in scripts/check-idris2-proofs.sh, not fixed.

Provenance note

This kernel was first drafted under the over-claiming name EveryType, which wrongly implied a universal "every type" relation and conflated the theory, the kernel, and a product profile in one repo. It is renamed anytype (pick any resource algebra, get that discipline). The theory now lives in systemet; the profile is AffineScript.

Verifiable anchor

Project

anytype

Repository

https://github.com/hyperpolymath/anytype

Commit (SHA)

<full commit SHA at time of signing>

Branch

main

Timestamp (UTC)

<ISO-8601 UTC timestamp>

Toolchain

<compilers / provers / versions used to ground the claims>

Affirmed by

Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>

Landed by a signed git commit. Verify with git log --show-signature that the anchor SHA above matches the commit that introduced this affirmation.