A Property Kind Calculus for Measurement Metrology

35.3. The contracts🔗

Three rubrics fix what a deployed unit is held to, and all three ask for the contract to be decidable rather than documented.

  • D3 — The data contract. The payload interface a unit reads and writes, declared, compiled into the executable, and validated against a producer's own claims before any payload is decoded. Checking after decoding is checking too late — by then a mis-channeled array has already been read as something it is not, and the failure surfaces as a wrong number rather than a rejection.

  • D4 — The platform contract. The argument plane the job scheduler passes, kind-typed and held to the registration payload, with the discharge relation between the two decided by the kernel rather than kept in step by hand. This is the seam where a deployment most often rots — the registration record and the executable's expectations drift apart across a rename — and it is the one seam where a machine-checked relation costs almost nothing.

  • D5 — A deployment card per unit. One deployment card per deployed unit, each panel read off a declared object. The card is the specification sheet of the deployment rather than of the model: the argument plane, the payload contract faces, the sizing, the knobs, the container facts. Its value comes entirely from being read off declarations, so that changing a contract either regenerates the card or fails.