FTS Proofs: Theorems, Certificates, and Scientific Boundaries

This is the most subtle module of the course. The word “proof” here means not what a business customer usually hears: FTS does not establish the truth of a business law, but checks two things — that the declared fact is indeed found in the data via an unambiguous path and that the morphism chain is typable. Everything else — are premises, and they are listed explicitly. The formulation “FTS proved that an order can be shipped” is incorrect. The correct formulation: “FTS checked the evidence and typability of the output under the condition of declared laws”.

Minimal example (theorem)

категория «Исполнение заказа»

  объект Заказ
    номер является строкой
    клиент является строкой
    оплачен является признаком
    «склад подтвердил» является признаком
    «готов к отгрузке» является состоянием «Готов к отгрузке»

  морфизм «Готовый заказ можно отгрузить»
    если «Готов к отгрузке»
    то «Отгрузить заказ разрешено»

  теорема «Заказ ЗК-7781 можно отгрузить»
    дано Заказ имеет «готов к отгрузке» равное да
    в данных заказы найти где номер равен «ЗК-7781»
    по морфизму «Готовый заказ можно отгрузить»
    следовательно «Отгрузить заказ разрешено»

Context — a regular JSON snapshot of data, not a part of the model:

{
  "заказы": [
    {
      "номер": "ЗК-7781",
      "клиент": "ООО Маяк",
      "оплачен": true,
      "склад подтвердил": true,
      "готов к отгрузке": true
    }
  ]
}

What the compiler does

compile turns the surface into a canonical document and already at this stage rejects part of the errors. The theorem unfolds into a proposition:

{
  "kind": "apply",
  "functor": "Готовый заказ можно отгрузить",
  "arg": {
    "kind": "witness",
    "structure": "Заказ",
    "field": "готов к отгрузке",
    "selector": { "номер": "ЗК-7781" },
    "value": true,
    "path": ["заказы", { "номер": "ЗК-7781" }, "готов к отгрузке"]
  }
}

The Russian surface parser checks: does the field exist, does the morphism exist, does the morphism domain match the type of the current step, and does the declared следовательно match the computed codomain. All four checks are syntactic and referential; there is no data at this stage yet. validate additionally controls names, duplicates, and referential integrity, but does not recalculate the type chain: for the Russian surface, this has already been done by the parser, and for the canonical JSON obtained in another way, by the certificate builder.

Proposition, witness and type

The Curry-Howard correspondence reads as follows: a type is a statement, a term of this type is a proof of the statement. prove prints both sides. The actual derivation on the model above:

{
  "curry_howard": {
    "proposition": "Готовый заказ можно отгрузить(Π (x:Заказ). готов к отгрузке(x))",
    "witness": "Готовый заказ можно отгрузить (λx. π_готов к отгрузке(x))"
  },
  "categorical": {
    "category": "Исполнение заказа",
    "morphism": "Готовый заказ можно отгрузить ∘ π_готов к отгрузке",
    "domain": "Заказ",
    "codomain": "Type"
  },
  "path": ["заказы", { "номер": "ЗК-7781" }, "готов к отгрузке"]
}

Walkthrough of the entry Готовый заказ можно отгрузить(Π (x:Заказ). готов к отгрузке(x)):

• Π (x:Заказ). готов к отгрузке(x) — assertion “for the order x defined field готов к отгрузке of declared type”. This assertion is about the presence of a certificate, not that all orders are ready for shipment;
• λx. π_готов к отгрузке(x) — witness of this assertion, field projection. The certificate is literal here: a specific value at a specific path;
• external application — this is the application of a morphism to a witness, that is, ordinary function application to an argument. The result type — codomain of the morphism.

Two disclaimers, without which the record is reevaluated. First: the line with Π and λ — readable notation output, not a term checked by the kernel with dependent types; FTS does not implement normalization and does not check λ-terms. Type equality is nominal, by name: «Готов к отгрузке» matches «Готов к отгрузке» and does not match anything else. Second: the codomain field in the prove output equals the string Type, not the conclusion type. The actual conclusion type appears only in the certificate, in the conclusion.type field — there it is «Отгрузить заказ разрешено».

Morphisms and Composition

The categorical part is minimal and therefore honest. Objects — types (Заказ, «Готов к отгрузке», «Отгрузить заказ разрешено»). Morphism — an arrow A → B with a name and a declared law. Composition — sequential application of arrows when the codomain of the previous matches the domain of the next.

These are precisely morphisms, not functors: a functor would map an entire category, along with its objects and arrows, preserving composition. A single transition A → B within one category is not a functor. In canonical JSON, the field historically is called functors, and a certificate step is apply with the field functor; this is a legacy from the first version of the wire format, fixed in the language documentation. The surface (морфизм) and the terminology of the research are corrected, the public API returns a representation morphisms() over the same field, and the format migration will be versioned.

Composing two morphisms on model credit-limit.fts gives the following derivation prove:

{
  "curry_howard": {
    "proposition": "(Пройденный скоринг открывает риск-проверку ∘ Успешная риск-проверка разрешает лимит) Π (x:Заявка на лимит). скоринг пройден(x)"
  },
  "categorical": {
    "morphism": "Пройденный скоринг открывает риск-проверку ∘ Успешная риск-проверка разрешает лимит",
    "domain": "Заявка на лимит",
    "codomain": "Type"
  }
}

Here is a reading trap: in the form compose the chain is printed in the order of declaration, left to right, whereas the mathematical ∘ is read right to left. In the form apply (a singleton morphism) the order is exactly standard: Готовый заказ можно отгрузить ∘ π_готов к отгрузке. The order of actual application is set by the list functors in the document, not by the rendered string.

Symbolic derivation

An important detail that can easily be mistaken for a bug. prove returns the same result with and without context: the path, proposition, and witness are derived from the document, not from the data. Context affects only one thing — when values do not match, prove throws FTS_WITNESS_MISMATCH. That is, the absence of an error from prove without context says nothing about the data.

Exact contract prove: it checks that the document is valid and that the evidence path resolves unambiguously to the expected value. The chain’s typability is not recalculated — it is checked by the compiler during theorem walkthrough and will be checked again during certificate construction.

Symbolic derivation is an inference schema: «if there exists a declared witness and the declared laws are true, then the conclusion is typified». It is useful at the stage of model design and is useless as a basis for action. In the certificate such an object is assigned status symbolic, and in assumptions a line of the form symbolic witness Заказ.готов к отгрузке : Готов к отгрузке is added.

Verified certificate

certify builds the certificate, verify independently rechecks it:

fts check order-shipment.fts
fts certify order-shipment.fts --context order-shipment.context.json --pretty > proof.json
fts verify order-shipment.fts --context order-shipment.context.json --certificate proof.json

Certificate for the model and a screenshot from the first section:

{
  "version": "fts-proof/1",
  "category": "Исполнение заказа",
  "status": "verified",
  "document_digest": "sha256:955d7f5d91674d9048a61dd2feedd28a76ae1aec70b3a3f4f8049383761a9829",
  "assumptions": [
    "Готовый заказ можно отгрузить : Готов к отгрузке → Отгрузить заказ разрешено [morphism.declared]"
  ],
  "steps": [
    {
      "rule": "witness",
      "structure": "Заказ",
      "field": "готов к отгрузке",
      "type": "Готов к отгрузке",
      "path": ["заказы", { "номер": "ЗК-7781" }, "готов к отгрузке"],
      "verified": true,
      "expected": true,
      "actual": true,
      "evidence_digest": "sha256:2b3351538d544658fcb6b9e59d8fc42e7de7593446c3303d8687f7d8ede15fae"
    },
    {
      "rule": "apply",
      "functor": "Готовый заказ можно отгрузить",
      "domain": "Готов к отгрузке",
      "codomain": "Отгрузить заказ разрешено",
      "law": "morphism.declared"
    }
  ],
  "conclusion": {
    "type": "Отгрузить заказ разрешено",
    "term": "Готовый заказ можно отгрузить(witness(Заказ.готов к отгрузке))"
  },
  "context_digest": "sha256:d0dc722124c5464cd0ccd5106f90fb9ed5da94be218e384488b13a287ff3096d",
  "certificate_digest": "sha256:58334701b7ba867d545524c5b6e0a6f4659bc288751f4c7a90a0fa3d0e73de68"
}

Status verified is assigned only if each witness is resolved in the context and the actual value matches the expected one. The morphism law remains in assumptions — the certificate does not assert it, but lists it.

Digest is calculated not from the JSON text, but from the canonical form: object keys are sorted by UTF-16 code units, array order is preserved, non-numeric values, infinities, and negative zero are rejected. Therefore, rearranging keys in the original snapshot gives the same context_digest and the same certificate_digest — this is verified experimentally and is a requirement of reproducibility, not an implementation detail.

What happens during substitution. verify does not compare strings, but rebuilds the output from the document and context, recalculates all digests, and compares them with the received ones. Changing any byte of data that enters the canonical snapshot changes context_digest, and through it — certificate_digest, and the check gives valid: false with a discrepancy between expected_digest and actual_digest. Pay attention: the status field in the result of the check describes the newly built output, not the received certificate. Strict mode (assertVerified, command fts verify) additionally requires status = verified and rejects a symbolic certificate with code FTS_CERTIFICATE_SYMBOLIC.

certify and verify use node:crypto and are not included in the browser build. The sandbox on the site can only prove: it is not possible to obtain a certificate in the browser due to the package structure. This is an intentional architectural limitation — issuing a certificate and authorizing an action belong to the trusted server boundary.

What This Does NOT Prove

• Truth of the business law. если «Готов к отгрузке» то «Отгрузить заказ разрешено» — is a premise, not a theorem. FTS proves a statement regarding the list assumptions, and this list cannot be removed.
• Completeness of the model. A morphism does not know about sanction lists, blocking a client, or overdue items. A correct conclusion based on an incomplete model remains a correct conclusion based on an incomplete model.
• Freshness of the snapshot. A certificate is tied to the state of data at the moment of issue. The world can change between verify and actual delivery.
• Authorship. SHA-256 links artifacts but does not confirm who issued them; a digital signature of the certificate is needed for that, which is absent in the current version.
• Absence of a defect in the implementation. A trusted base — a normalizer, core rules, canonizer, and verifier. An error in them is not detected by the certificate.
• Rich type system. Type equality is nominal; there are no parametric or dependent types.

Separately on the scientific and patent status. In the research materials of the project meta-properties (determinism of path resolution, uniqueness of type inference, type preservation, termination of checking, relative correctness, detection of certificate modification) are formulated and proved by induction — but for the publication level this is insufficient. A separate formal layer is needed: operational semantics, typing judgments, selected safety properties with proofs, reference implementation, replication package and benchmark.

For a patent the situation is stricter. One cannot claim as new either the Curry-Howard correspondence, or categorical composition, or static typing, or JSON Schema, or cryptographic hash, or proof-carrying code, or agent tool invocation. A potentially patentable might be a specific combination of features and the achieved technical result, and a conclusion about novelty is permissible only after patent and bibliographic search. Public disclosure before filing an application in a number of jurisdictions destroys novelty, therefore the correct order is search of the prior art, consultation with a patent attorney, filing, publication. The FTS certificate — a good object of study and machine-checkable evidence, but not a patent examination.

Practice in the sandbox

Single morphism and derivation walkthrough prove:

Composition of two morphisms — compare morphism and the application order:

Diagram of the same category — objects and arrows without the proof part:

Recall: only prove is available in the sandbox. There are no status, assumptions, or digests there — they appear in the output of fts certify in Node.js.

Common Fallacies

• FTS_WITNESS_MISMATCH — «witness does not match context at заказы[номер="ЗК-7781"].готов к отгрузке: expected true, got false». Witness found, but the value is different. This is not a model error: it means, that based on the data the order cannot be shipped.
• FTS_WITNESS_MISMATCH with got <missing> — the path did not resolve. Three different reasons give one message: the element does not exist, the root key is named differently, or the selector matched more than one element. The implementation requires exactly one match, so a duplicate number in the snapshot looks like missing data.
• FTS_PROOF_TYPE_MISMATCH — «morphism «Paid order can be shipped» expects «Payment confirmed», got «Ready for shipping»». It appears already at compilation, before any data.
• FTS_UNKNOWN_FUNCTOR — «morphism «…» not found»: the theorem refers to an arrow, which does not exist in the category.
• FTS_THEOREM_CONCLUSION — «the theorem declares «Invoice can be issued», but the output has the type «Shipment of order is allowed»». The declared conclusion did not match with the codomain of the last morphism.
• FTS_CERTIFICATE_SYMBOLIC — strict check received a certificate without a confirmed witness.
• FTS_CERTIFICATE_MISMATCH — certificate does not match the document and context: the data, the model or the certificate itself have changed.

Checklist

1. The theorem’s conclusion coincides with the codomain of the last morphism — otherwise the model will not compile.
2. The evidence selector chooses exactly one element; the snapshot contains a stable identifier.
3. To resolve the action, fts verify with status verified is used; symbolic action does not resolve.
4. The list assumptions is read aloud and accepted by the person responsible for the business rule, not the developer.
5. Along with the decision, the source, context, and certificate are saved — otherwise the check cannot be repeated.
6. In formulations for the customer, instead of “it is proven that the order can be shipped,” it is stated “the evidence and typability of the output are checked under the condition of declared laws.”

Cases in the catalog on this topic

Next: integration with any language