Mental model: data, rules, inference, and effect

This chapter sets the vocabulary for the whole course: how to read a flang file without confusing four different things that ordinary code piles into one method. Once this separation sinks in, the later chapters are details of the same four layers.

Minimal example

модуль «Исполнение заказа»

объект «Заказ»
  «номер»: строка
  «оплачен»: признак
  «склад подтвердил»: признак

тотальная функция «Можно отгрузить»
  принимает заказ: «Заказ»
  возвращает признак
  обеспечивает «неоплаченный заказ не отгружается» если не заказ.«оплачен» то результат равен нет иначе да
  пример «оплачен, но склад молчит»
    дано заказ равно запись «Заказ» с «номер» равным "ЗК-7781" и «оплачен» равным да и «склад подтвердил» равным нет
    ожидается нет
  если заказ.«оплачен»
    то заказ.«склад подтвердил»
    иначе нет

All four layers are visible at once. объект «Заказ» is data. The function «Можно отгрузить» is a rule. The обеспечивает line is a promise the compiler proves for every order. And the fact that the order actually leaves the warehouse happens outside, in the warehouse code, and only if the rule said “yes”.

The fourth step is inference on real data. The facts go into JSON, the claim is written in words:

$ flang facts shipment.flang --facts order.json --claims '["«Можно отгрузить» от заказ равно да"]'

For an order that is paid but not confirmed by the warehouse, the answer is this (the steps field with the evaluation steps is omitted):

{
  "ok": false,
  "results": [
    {
      "claim": "«Можно отгрузить» от заказ равно да",
      "holds": false,
      "why": "«Можно отгрузить» от факта «заказ» = нет, а утверждение требует «равно да». Исходные факты — «заказ»: номер = «ЗК-7781», оплачен = да, склад подтвердил = нет",
      "status": "refuted"
    }
  ]
}

The exit code is 1: the claim is refuted, and the answer names the facts it was derived from.

What the compiler does

flang check parses the file, checks the types, proves termination of every тотальная function and evaluates every пример. The --proof flag adds a proof report: for each promise, whether it is proved and by what.

flang facts evaluates claims on facts. It only lets you call functions with proved termination, so an answer always comes: the evaluation cannot hang.

None of the commands goes to the network or reads files beyond those named in the arguments. The model and the facts are always passed explicitly.

Four layers

Data. объект describes the shape of the input: a set of named fields with types. There are no methods, constructors or hidden state — it is not a class. When a value comes in different kinds (an order is “created”, “paid”, “shipped”), you declare a тип with variants, and taking it apart must cover every variant.

Rules. A rule is a тотальная функция: input → decision. It does not change data and knows nothing about time, the network or the database. Its behaviour on specific inputs is written as examples, and on all inputs as обеспечивает promises.

Inference. Two kinds. A promise proved by the compiler is a statement about all inputs. flang facts is a statement about one specific data set: can this order be shipped right now or not, and why.

Effect. Charging money, writing to the database, a command to the warehouse happen outside the model. The compiler can answer “shipment allowed” or compute a discount, but it does nothing in the outside world itself.

The effect boundary is drawn on purpose. A model function cannot open a file or a socket: in flang an action on the world is a value that describes it (план), executed by the program that started it. So the same file gives the same result in the sandbox, in Node.js and in CI. When exactly a decision turns into an action is up to the application: retries, idempotency and message queues are the job of the code that received the answer.

Calculation and guard — two kinds of rules

A calculation rule returns a number: a discount, a tariff, a bonus. It is checked by examples and by promises such as “the discount is at most 15,000”.

A guard rule returns a flag (да/нет) or a type with variants like “Allowed / Refused with a reason”. Its main promise is an implication: “if the order is not paid, the answer is no”. The compiler proves such promises by itself, from the condition of the если branch, without a single theorem.

An ordinary TypeScript function can do the same computation. The difference is that a model function physically cannot touch the network or a file and cannot hang, and its promises are checked before it runs. An ordinary function guarantees this only through the team’s discipline.

Three levels of confidence

The flang check --proof report names each promise with one of three words, and they are not interchangeable:

• “доказано” (proved) — true for all inputs. Exit code 0;
• “сетка N” — checked only on the author’s N examples. It is not a proof. Exit code 3;
• “объявлено, не доказано” (declared, not proved) — neither a proof nor examples. Exit code 3.

Here is a function with a bug in its body: it answers “yes” to an unpaid order.

модуль «Исполнение заказа»

объект «Заказ»
  «номер»: строка
  «оплачен»: признак
  «склад подтвердил»: признак

тотальная функция «Можно отгрузить»
  принимает заказ: «Заказ»
  возвращает признак
  обеспечивает «неоплаченный заказ не отгружается» если не заказ.«оплачен» то результат равен нет иначе да
  пример «оплачен, но склад молчит»
    дано заказ равно запись «Заказ» с «номер» равным "ЗК-7781" и «оплачен» равным да и «склад подтвердил» равным нет
    ожидается нет
  если заказ.«оплачен»
    то заказ.«склад подтвердил»
    иначе да

$ flang check shipment-wrong.flang
модуль «Исполнение заказа»: функций 1, из них с доказанным завершением 1; типов 1
shipment-wrong.flang: проверено — разбор, типы, завершаемость, ядро и примеры; замечаний нет

$ flang check shipment-wrong.flang --proof
  постусловие «неоплаченный заказ не отгружается» функции «Можно отгрузить» — сетка 1 значение (примеры функции): нарушений НЕ ИСКАЛИ — прогона примеров не было, посчитано только их число. Это не доказательство — теоремы при утверждении нет
shipment-wrong.flang: НЕ ДОКАЗАНО — ОПОРА НЕ СУДИЛАСЬ — утверждений 1: доказано 0, условно 0, сетка 1, объявлено, не доказано 0, отвергнуто 0, нарушено 0; законов на сетке 0, на веру 0 — код возврата 3

This is the main lesson of the chapter. Without --proof the answer is green: no example refutes the promise. With --proof you see it is not proved — code 3. The lie is not caught yet, but it is not passed off as truth either.

An example on the right branch catches it:

модуль «Исполнение заказа»

объект «Заказ»
  «номер»: строка
  «оплачен»: признак
  «склад подтвердил»: признак

тотальная функция «Можно отгрузить»
  принимает заказ: «Заказ»
  возвращает признак
  обеспечивает «неоплаченный заказ не отгружается» если не заказ.«оплачен» то результат равен нет иначе да
  пример «оплачен, но склад молчит»
    дано заказ равно запись «Заказ» с «номер» равным "ЗК-7781" и «оплачен» равным да и «склад подтвердил» равным нет
    ожидается нет
  пример «неоплаченный заказ»
    дано заказ равно запись «Заказ» с «номер» равным "ЗК-7782" и «оплачен» равным нет и «склад подтвердил» равным да
    ожидается да
  если заказ.«оплачен»
    то заказ.«склад подтвердил»
    иначе да

$ flang check shipment-wrong.flang
модуль «Исполнение заказа»: функций 1, из них с доказанным завершением 1; типов 1
FLANG_EXAMPLE: пример «неоплаченный заказ» функции «Можно отгрузить»: FLANG_PROPERTY: нарушено свойство «неоплаченный заказ не отгружается» функции «Можно отгрузить»
shipment-wrong.flang: не проверено — замечаний 1

No level makes a business rule true “out of thin air”. The compiler proves that the code keeps the promise. Whether the promise itself is right is decided by policy, a contract or the owner of the rule.

Sandbox practice

Find the two proved promises of the function «Можно отгрузить» in the report. Change иначе нет to иначе да in its body. Both promises become “сетка 2”: the compiler no longer derives them from the new body, and they rest only on two examples.

Add an example to «Рассчитать скидку» with an amount of exactly 10000 and no regular customer. Work out the expected number by hand from the function «Большая покупка» and make all examples pass.

There are two steps in a row here: «Риск-проверка разрешена» and «Лимит может быть установлен». Find the promise «без скоринга лимита нет» and explain why the compiler proved it, although it rests on the result of another function.

Common mistakes

FLANG_EXAMPLE — an example evaluated to a different value than it expects. The message names the example, the function and both values: значение не совпало с ожидаемым: ожидалось true, получено false. The fix is to correct the body or the expectation; whoever knows the rule decides.

Taking code 3 for success. flang check without --proof does not ask about proofs and answers 0 even for a false promise if the examples did not hit it. CI needs flang check --proof, and code 3 there is not green.

Taking "holds": false for a failure. Code 1 from flang facts means “refuted”, not “broken”. A failed call is code 2. A refuted claim is a normal answer: for example, a refused shipment.

Checklist

• I can split any rule of my system into data, rule, inference and effect — separately.
• I tell a calculation rule from a guard rule and know which promises the compiler proves by itself.
• I read the --proof report and do not confuse “доказано”, “сетка N” and “объявлено, не доказано”.
• I explain why the effect boundary is a decision of the application, not of the language.

Catalogue cases on this topic

Next: tools and JSON