FTS Mental Model: Data, Rules, Inference, and Effect

This chapter sets the glossary for the entire course: how to read a .fts file, without confusing four different things that in ordinary code are usually lumped into one method. If this separation is absorbed, further chapters are just new syntax for the same four layers.

Minimal example

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

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

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

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

Here all four layers are visible at once: объект — data, морфизм — rule, теорема — inference, and the fact that the order was actually shipped will happen externally, in the warehouse code.

What the compiler does

compile(source) builds one canonical FtsDocument — a flat JSON with fields category, structures, functors, proposition, utilities. validate(document) checks that names are not duplicated, object fields exist, and the domain and codomain of each morphism are real evidence types. Three paths diverge further: prove builds human-readable output from proposition and, if given a JSON context, matches witness with real data; certify/verify do the same, but with SHA-256 digests for independent verification; testUtilities executes пример-blocks inside утилита as executable tests. None of these steps reads the file itself — source and context are always passed explicitly, as arguments.

Four Layers

Data. объект and структура describe the observable form of input: a set of named fields with a type. There are no methods, constructors, or hidden state — this is not a class.

Rules. Two different kinds. правило inside утилита — deterministic transformation of the result: if the condition is true, the action changes the number. морфизм — a permissible transition between evidence types, without computing the number: it either allows the transition or not.

Conclusion. теорема links a specific data fact to one or more morphisms and checks that the declared consequence indeed follows through the chain. пример inside the utility — the same principle for computations: a specific input must yield the declared result, otherwise the compiler rejects the model at fts test.

Effect. Money charge, record in the database, sending a command to the warehouse — all this happens outside FTS. The compiler can return “transition allowed” or a discount number, but performs nothing itself in the external world.

The boundary of the effect is drawn not because the language lacks something, but intentionally: FTS does not have HTTP, SQL, transaction, time, or randomness primitives, so the same .fts-file produces the same result in the browser, in Node.js, and in the CI test. The decision of when exactly the result becomes a real action is an architectural decision of the application, not the language. FTS does not know about retry, idempotency, or message queue; this is the work of the code that receives its result.

Morphism and utility — two different kinds of rules

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

Morphism describes a typed transition that is allowed, not arbitrary code. It is needed when it is important to show the inference chain: from which evidence the permission was obtained, not to count the number. A functor would map an entire category into another; for one rule it is not needed — in the current applied core, FTS functors are used as an internal representation of morphisms, and the term “functor” does not appear in the user syntax.

A utility differs from a regular function in code in three ways. First, it must have an explicit начинает с — there is no implicit undefined or null at the beginning of the computation. Second, the rules inside it are not if / else if with side effects, but a named list: all rules whose conditions are true are executed, and the order affects only the order in which values are accumulated. Third, a utility physically cannot access the network or files — its grammar simply has no such constructs. A TypeScript function can do all of the above, and this is why it does not replace the utility as a source of truth: a compiled .fts guarantees what a regular function guarantees only through team discipline.

Three Confidence Levels

• fts check proves only the structural and type correctness of the model.
• fts test demonstrates that the utility’s executable examples match the current semantics.
• fts verify recalculates the certificate independently and checks that each witness resolved in a specific JSON context.

No stage makes an external business law true “out of thin air.” If a team declares a morphism “successful check authorizes payment,” FTS will check its correct application and show the law as an explicit premise in the certificate (assumptions), but the basis of this law is a policy, a contract, or research, not the compiler.

Practice in the sandbox

Find assumptions and steps in the output: which line is the data, which is the applied morphism, and which is the final conclusion. Then open diagram of the same file and compare it with the textual output.

Add the sixth пример with a total of exactly 10000 and without a regular customer. Calculate the expected result manually according to the “Big Purchase” rule and achieve 6/6 examples.

Here are two morphisms in a row. Define the domain and codomain of each and explain why the codomain of the first must match the domain of the second — otherwise the chain of derivation will not assemble.

Common Fallacies

FTS_NATURAL_DECLARATION — the compiler expected one of five top-level category keywords: объект, структура, морфизм, теорема, or утилита. If you write, for example, функция «Что-то» instead of утилита «Что-то», you will get exactly this diagnostic with the line indicated. Fix — use one of the allowed keywords.

FTS_WITNESS_MISMATCH — declared in дано value did not match the real data at the specified path. For the example above, if the order «готов к отгрузке» is actually нет, prove will return: witness does not match context at заказы[номер="ЗК-7781"].готов к отгрузке: expected true, got false. This is not a syntax error — the model is correct, but the fact is in another context. Fix — correct either the data or the theorem condition; the persuasiveness of the rule text does not affect this.

Checklist

• I can decompose any rule of my system into data, rule, inference, and effect — separately.
• I understand the difference between морфизм (valid transition) and правило (utility) (number calculation).
• I know that fts check, fts test, and fts verify prove different things and do not replace each other.
• I explain why the effect boundary is an application decision, not a language one.

Cases in the catalog on this topic

Next: installation and JSON