Antipatterns: what should not be expressed as a specification

A language that can do less makes fewer mistakes. But the saving only works when the boundary is known in advance: otherwise the first two weeks go into attempts to write what cannot live in a model, and into the verdict “the tool is raw”. The mistakes below are not carelessness. They are exactly the constructs written by someone with fifteen years of imperative code behind them: there a function means an action, a field may come from the network, and a green build means “correct”. In flang each of these assumptions is wrong in its own way.

How to read this catalog

Each item follows one scheme: what the task really is, how people try to write it, what the compiler answers, and what a working split looks like. The third step matters more than the rest. Some attempts the compiler refuses at once — that is a good outcome. Some pass the check, and a model that is green but does not mean what its author meant costs more than any diagnostic.

All answers were produced by the flang 0.7.29 binary. Programs marked as errors fail the check on purpose; the rest pass flang check --proof and flang test — you can paste them into the sandbox as they are.

Effects in a specification

1. An action inside a function

Task. On a large purchase, email the customer a promo code.

модуль «Письма»

объект «Покупка»
  «сумма»: неотрицательное
  «почта»: строка

тотальная функция «Большая покупка»
  принимает покупка: «Покупка»
  возвращает число
  если покупка.«сумма» не меньше 10000
    то отправить письмо на покупка.«почта»
    иначе 0

What happens. The check fails:

FLANG_UNKNOWN_NAME в файле a1.flang, строка 11, столбец 8: имя «отправить» не связано: имя вводят 'принимает', 'пусть' или образец 'случай'; а действия языка ('плюс', 'минус', 'умножить на', 'делить на', 'остаток от') пишутся МЕЖДУ значениями — «3.14 умножить на р», а не «умножить 3.14 на р»

There is no verb «отправить» (send) in the language, and you cannot invent one: a flang function computes a value and does nothing else. The network, files and processes are out of its reach.

The right way. Decision and action are split. A function answers “is a letter due”, and the sending is described by a план (plan): a function returns a command («Запросить» — an HTTP request to the mailing service), the host runs it (flang io), and the answer comes back into the same function. The logic stays pure and is checked by examples without any network:

модуль «Письмо о промокоде»

объект «Покупка»
  «сумма»: неотрицательное
  «почта»: строка

тотальная функция «Нужно письмо с промокодом»
  принимает покупка: «Покупка»
  возвращает признак
  обеспечивает «мелкой покупке письма нет» если покупка.«сумма» меньше 10000 то результат равен нет иначе да
  пример «на десять тысяч письмо положено»
    дано покупка равно запись «Покупка» с «сумма» равным 10000 и «почта» равным "a@example.org"
    ожидается да
  если покупка.«сумма» меньше 10000
    то нет
    иначе да

тип «Ход»
  вариант «Отправляем»
  вариант «Ждём ответа»

план «Отправить письмо»
  состояние «Ход»
  начинает с «Начало»
  обрабатывает «Дальше»

тотальная функция «Начало»
  возвращает «Ход»
  вариант «Отправляем»

тотальная функция «Дальше»
  принимает ход: «Ход», отклик: «Отклик»
  возвращает «Продолжение»
  пример «первым делом уходит запрос к службе рассылки»
    дано ход равно вариант «Отправляем»
    дано отклик равно вариант «Пока ничего»
    ожидается вариант «Сделать» с поручение равным (вариант «Запросить» с способ равным "POST" и адрес равным "http://127.0.0.1:8025/send" и тело равным "промокод") и потом равным (вариант «Ждём ответа»)
  пример «служба ответила — план закончен»
    дано ход равно вариант «Ждём ответа»
    дано отклик равно вариант «Ответ сети» с код равным 202 и тело равным "принято"
    ожидается вариант «Конец работы» с значение равным "принято"
  разбор ход
    случай вариант «Отправляем»
      то вариант «Сделать» с поручение равным (вариант «Запросить» с способ равным "POST" и адрес равным "http://127.0.0.1:8025/send" и тело равным "промокод") и потом равным (вариант «Ждём ответа»)
    случай вариант «Ждём ответа»
      то разбор отклик
        случай вариант «Ответ сети» с код как код и тело как тело
          то вариант «Конец работы» с значение равным тело
        случай вариант «Сбой» с код как код и сообщение как сообщение
          то вариант «Провал» с код равным код и сообщение равным сообщение
        случай любое
          то вариант «Провал» с код равным "FLANG_IO_ORDER" и сообщение равным "ждали ответ сети"

The promise «мелкой покупке письма нет» (no letter for a small purchase) is proved here for all inputs, and both steps of the plan are covered by examples. The letter template, retrying when the service fails and the delivery report stay in the mailing service: the compiler checks none of them.

2. An action hidden in a name

More dangerous is the variant where the code has no effect and only the name does.

модуль «Уведомления»

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

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

What happens. Nothing: the model passes the check, there are no diagnostics. The trap is the name — it states an accomplished fact, and a month later someone will read да as confirmation that the letter went out. The function says something else: the order is paid. Nobody checked the sending.

The right way. A function name states a permission or an obligation: «Нужно уведомить клиента» (the customer must be notified). The fact of sending comes back from the mailing system into the data and becomes a field of an object — then something can be claimed about it.

3. Retries, timeouts, queues

Task. After a payment failure retry in five seconds, then in thirty, and after that stop retrying.

There is no waiting, scheduling or queue in the language: ждать 5 секунд gives the same FLANG_UNKNOWN_NAME as in item 1.

The right way. Separate “how long to wait” from “who waits”. The retry policy is a pure table worth pinning down; executing the delay, the idempotency key and deduplication stay in the application.

модуль «Повторы платежа»

объект «Неудачная попытка»
  «номер попытки»: неотрицательное
  «ошибка окончательная»: признак

тип «Повтор»
  вариант «Повторить через» содержит секунд: неотрицательное
  вариант «Не повторять»

тотальная функция «Следующий повтор»
  принимает попытка: «Неудачная попытка»
  возвращает «Повтор»
  пример «после первой попытки ждём пять секунд»
    дано попытка равно запись «Неудачная попытка» с «номер попытки» равным 1 и «ошибка окончательная» равным нет
    ожидается вариант «Повторить через» с секунд равным 5
  пример «окончательная ошибка не повторяется»
    дано попытка равно запись «Неудачная попытка» с «номер попытки» равным 1 и «ошибка окончательная» равным да
    ожидается вариант «Не повторять»
  пример «третья попытка не назначается»
    дано попытка равно запись «Неудачная попытка» с «номер попытки» равным 3 и «ошибка окончательная» равным нет
    ожидается вариант «Не повторять»
  если попытка.«ошибка окончательная»
    то вариант «Не повторять»
    иначе если попытка.«номер попытки» равен 1
      то вариант «Повторить через» с секунд равным 5
      иначе если попытка.«номер попытки» равен 2
        то вариант «Повторить через» с секунд равным 30
        иначе вариант «Не повторять»

«Не повторять» (do not retry) is a separate variant of the answer here, not zero seconds. The application must handle both cases and cannot mistake a refusal for “retry right away”.

The outside world: time, randomness, network

4. An external source as a field

Task. Recompute the tariff by the current exchange rate from an external API.

модуль «Тарифы»

объект «Отправление»
  «вес»: неотрицательное
  «курс валюты» является запросом

What happens.

FLANG_UNKNOWN_NAME в файле a4.flang, строка 3, столбец 1: неизвестный тип «запросом»

A field only ever has a declared type: a built-in one (число, строка, признак, неотрицательное) or your own, introduced with тип or объект. An unknown word after является is an error, not a new type. The earlier FTS surface accepted such a word silently; flang refuses at once.

The right way. The application fetches the rate — with a timeout, a cache and a fallback value. It reaches the model as an ordinary field «курс валюты»: число.

5. “Today” inside a rule

Task. Charge a penalty when an invoice is overdue relative to today.

модуль «Пени»

объект «Счёт»
  «срок оплаты»: неотрицательное

тотальная функция «Просрочен»
  принимает счёт: «Счёт»
  возвращает признак
  счёт.«срок оплаты» меньше сегодня

What happens.

FLANG_UNKNOWN_NAME в файле a5.flang, строка 9, столбец 29: имя «сегодня» не связано: имя вводят 'принимает', 'пусть' или образец 'случай'; а действия языка ('плюс', 'минус', 'умножить на', 'делить на', 'остаток от') пишутся МЕЖДУ значениями — «3.14 умножить на р», а не «умножить 3.14 на р»

The language has no clock, and that is not an omission: a function that answers one thing today and another tomorrow cannot carry examples. There is no date type in flang 0.7.29 either.

The right way. The application computes time and passes it in as data — here as a day number (days since 1 January 1970), so the comparison is a plain comparison of numbers:

модуль «Пени»

объект «Счёт»
  «сумма»: неотрицательное
  «день срока оплаты»: неотрицательное

тотальная функция «Дней просрочки»
  принимает счёт: «Счёт», сегодня: неотрицательное
  возвращает число
  обеспечивает «до срока просрочки нет» если сегодня не больше счёт.«день срока оплаты» то результат равен 0 иначе да
  пример «в день срока просрочки ещё нет»
    дано счёт равно запись «Счёт» с «сумма» равным 10000 и «день срока оплаты» равным 20650
    дано сегодня равно 20650
    ожидается 0
  пример «три дня после срока»
    дано счёт равно запись «Счёт» с «сумма» равным 10000 и «день срока оплаты» равным 20650
    дано сегодня равно 20653
    ожидается 3
  если сегодня не больше счёт.«день срока оплаты»
    то 0
    иначе сегодня минус счёт.«день срока оплаты»

The promise «до срока просрочки нет» (no overdue days before the due date) is proved for all inputs. An example with a specific day reproduces a year later exactly as today, and a disputed penalty can be reviewed after the fact.

6. Randomness: A/B tests, sampling, a random discount

Task. Give half of the customers a discount and compare conversion.

модуль «Эксперимент»

тотальная функция «Скидка по жребию»
  принимает сумма: неотрицательное
  возвращает число
  если случайное число меньше 0.5
    то (сумма умножить на 5) делить на 100
    иначе 0

What happens. FLANG_UNKNOWN_NAME в файле a6.flang, строка 6, столбец 8: имя «случайное» не связано. The language has no random numbers.

The right way. The application draws the lot — once, deterministically from the customer id — and stores the group. The group reaches the model as a variant:

модуль «Эксперимент»

тип «Группа»
  вариант «Контроль»
  вариант «Скидка пять процентов»

тотальная функция «Скидка эксперимента»
  принимает сумма: неотрицательное, группа: «Группа»
  возвращает число
  пример «контрольная группа без скидки»
    дано сумма равно 2000
    дано группа равно вариант «Контроль»
    ожидается 0
  пример «опытная группа получает пять процентов»
    дано сумма равно 2000
    дано группа равно вариант «Скидка пять процентов»
    ожидается 100
  разбор группа
    случай «Контроль»
      то 0
    случай «Скидка пять процентов»
      то (сумма умножить на 5) делить на 100

The group becomes part of the input: an example for every branch of the experiment is written just like any other.

Rule logic

7. Overlapping rules add up

Task. Five percent off from one thousand roubles, ten percent from ten thousand. Out of old habit the rules are split into functions and summed.

модуль «Скидка по ступеням»

объект «Покупка»
  «сумма»: неотрицательное

тотальная функция «От тысячи»
  принимает покупка: «Покупка»
  возвращает число
  если покупка.«сумма» не меньше 1000
    то (покупка.«сумма» умножить на 5) делить на 100
    иначе 0

тотальная функция «От десяти тысяч»
  принимает покупка: «Покупка»
  возвращает число
  если покупка.«сумма» не меньше 10000
    то (покупка.«сумма» умножить на 10) делить на 100
    иначе 0

тотальная функция «Скидка»
  принимает покупка: «Покупка»
  возвращает число
  пример «крупная покупка»
    дано покупка равно запись «Покупка» с «сумма» равным 20000
    ожидается 2000
  («От тысячи» от покупка) плюс («От десяти тысяч» от покупка)

What happens.

FLANG_EXAMPLE: пример «крупная покупка» функции «Скидка»: значение не совпало с ожидаемым: ожидалось 2000, получено 3000

At an amount of 20000 both conditions are true, and the contributions add up: 1000 plus 2000. Adding functions is addition, not choice. Here the example caught the error; without it the model would be green.

The right way. Mutual exclusion is expressed by a single если … иначе если chain: the branches are tried in order, and exactly one runs.

модуль «Скидка по ступеням»

объект «Покупка»
  «сумма»: неотрицательное

тотальная функция «Скидка»
  принимает покупка: «Покупка»
  возвращает число
  пример «крупная покупка»
    дано покупка равно запись «Покупка» с «сумма» равным 20000
    ожидается 2000
  пример «средняя покупка»
    дано покупка равно запись «Покупка» с «сумма» равным 5000
    ожидается 250
  пример «ровно тысяча»
    дано покупка равно запись «Покупка» с «сумма» равным 1000
    ожидается 50
  если покупка.«сумма» не меньше 10000
    то (покупка.«сумма» умножить на 10) делить на 100
    иначе если покупка.«сумма» не меньше 1000
      то (покупка.«сумма» умножить на 5) делить на 100
      иначе 0

Summing rule contributions is legitimate when that is the business rule: “five percent for a regular customer on top of the volume discount”. Then name the functions that way and cover the sum with an example where they overlap.

8. An если chain over the kind of a value instead of разбор

Task. Allow shipping an order based on its status.

модуль «Статусы»

тип «Статус»
  вариант «Создан»
  вариант «Оплачен»
  вариант «Готов к отгрузке»
  вариант «Отменён»

тотальная функция «Можно отгрузить»
  принимает статус: «Статус»
  возвращает признак
  пример «отменённый не отгружается»
    дано статус равно вариант «Отменён»
    ожидается нет
  если статус равен вариант «Создан»
    то нет
    иначе если статус равен вариант «Оплачен»
      то нет
      иначе да

What happens.

FLANG_EXAMPLE: пример «отменённый не отгружается» функции «Можно отгрузить»: значение не совпало с ожидаемым: ожидалось false, получено true

The cancelled order slipped silently into the last иначе and was allowed to ship. The example caught it; a new status variant added half a year later will have nothing to catch it.

The right way. A choice by the kind of a value is written with разбор: the compiler requires every variant to be named. The same code with a forgotten variant:

модуль «Статусы»

тип «Статус»
  вариант «Создан»
  вариант «Оплачен»
  вариант «Готов к отгрузке»
  вариант «Отменён»

тотальная функция «Можно отгрузить»
  принимает статус: «Статус»
  возвращает признак
  разбор статус
    случай «Создан»
      то нет
    случай «Оплачен»
      то нет
    случай «Готов к отгрузке»
      то да

FLANG_MATCH_NOT_EXHAUSTIVE в файле a8b.flang, строка 12, столбец 3: разбор «Статус» не покрывает «Отменён»

The missed case shows up at check time, not with a person at the warehouse.

9. A promise kept by clipping

Task. Cap the discount at fifteen thousand.

модуль «Потолок скидки»

объект «Покупка»
  «сумма»: неотрицательное
  «постоянный клиент»: признак

тотальная функция «Скидка»
  принимает покупка: «Покупка»
  возвращает число
  обеспечивает «скидка не больше пятнадцати тысяч» результат не больше 15000
  пример «покупка на сто тысяч постоянного клиента»
    дано покупка равно запись «Покупка» с «сумма» равным 100000 и «постоянный клиент» равным да
    ожидается 20000
  если покупка.«постоянный клиент»
    то (покупка.«сумма» умножить на 20) делить на 100
    иначе (покупка.«сумма» умножить на 15) делить на 100

What happens. A promise обеспечивает does not fix the result, it checks it. The example at one hundred thousand honestly fails:

FLANG_EXAMPLE: пример «покупка на сто тысяч постоянного клиента» функции «Скидка»: FLANG_PROPERTY: нарушено свойство «скидка не больше пятнадцати тысяч» функции «Скидка»

That is how it should be: the rules computed 20 000, the business promised no more than 15 000 — that is a finding. The tempting move is to add clipping to the body:

модуль «Потолок скидки»

объект «Покупка»
  «сумма»: неотрицательное
  «постоянный клиент»: признак

тотальная функция «Скидка по правилам»
  принимает покупка: «Покупка»
  возвращает число
  если покупка.«постоянный клиент»
    то (покупка.«сумма» умножить на 20) делить на 100
    иначе (покупка.«сумма» умножить на 15) делить на 100

тотальная функция «Скидка»
  принимает покупка: «Покупка»
  возвращает число
  обеспечивает «скидка не больше пятнадцати тысяч» результат не больше 15000
  пример «покупка на сто тысяч постоянного клиента»
    дано покупка равно запись «Покупка» с «сумма» равным 100000 и «постоянный клиент» равным да
    ожидается 15000
  если («Скидка по правилам» от покупка) не больше 15000
    то «Скидка по правилам» от покупка
    иначе 15000

Now the answer is flawless:

постусловие «скидка не больше пятнадцати тысяч» функции «Скидка» — доказано сведением цели с телом функции: правило «разбор цели по условию», объявленные типы аргументов не понадобились — утверждение обо ВСЕХ входах, а не о написанных; теоремы при нём нет и не нужно

Proved — and meaningless. The promise has become a repetition of the body: the rules still compute 20 % where the business expects at most 15 000, and the clipping hides it. The rule error moved from the report into silence.

The right way. The cap belongs in the rules themselves (as a separate “very large purchase” branch, as in order-discount.flang), and the promise stays a check: if the rules break it, the owner of the rule must find out, not если … то 15000. The same goes for tautologies like результат равен (0 минус х) with the body 0 минус х: such a promise is accepted for free and checks nothing.

Examples and proofs

10. A model without examples

модуль «Без примеров»

тотальная функция «Скидка»
  принимает сумма: неотрицательное
  возвращает число
  обеспечивает «скидка не больше десятой части» результат не больше (сумма делить на 10)
  если сумма не меньше 10000
    то (сумма умножить на 10) делить на 100
    иначе 0

What happens. The bare check is green:

a10.flang: проверено — разбор, типы, завершаемость, ядро и примеры; замечаний нет

The proof report tells the truth:

постусловие «скидка не больше десятой части» функции «Скидка» — объявлено, не доказано: ни теоремы, ни примеров. Его считает рантайм после каждого возврата — на тех входах, которые придут

and flang check --proof exits with code 3. A promise without an example is only checked at run time — on whatever inputs users happen to send. Text becomes a specification when it contains numbers the business agreed on: at least one example per branch and one per boundary.

11. An example fitted to the implementation

The quietest way to devalue the construct. Go back to item 7: the example honestly expects 2000, the function gives 3000, the check is red.

Then comes the fork. The right move is to fix the rules: the mismatch is the finding. The tempting one is to change it to ожидается 3000: CI is green, the commit is tiny. After that the example stops being a requirement and becomes a snapshot of behaviour. The model computes something other than what was promised to the customer, but now nobody will ever find out.

A code review rule: changing an ожидается line in the same commit as the rules counts as changing an agreement with the business and requires a link to its source — a ticket, an order, a tariff. No link — send it back.

12. Code 0 or an answer on facts passed off as proof

Task. Show an auditor that the discount model keeps its cap and that order ЗК-7781 may be shipped.

What happens. CI runs flang check, it is green — and that is read as “proved”. On the course model order-discount.flang:

static/spec/models/order-discount.flang: проверено — разбор, типы, завершаемость, ядро и примеры; замечаний нет

Without the --proof key not a word is said about proofs. With it:

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

“Сетка 5 значений” (a grid of five values) means the cap was checked on five examples, like five unit tests. It is not proved for all inputs.

The second substitution is an answer from flang facts on the data of a single order. The claim “the order with this number ships” holds on order-shipment.facts.json: "holds": true, "status": "verified". That is a fact about one order in one data snapshot, not a rule. The rule is the promises of the function «Можно отгрузить» («неоплаченный заказ не отгружается» — an unpaid order does not ship), and for those the report says “proved” — for all orders.

The right way. CI runs flang check --proof, and code 3 does not count as green. The auditor gets the proof report line for each promise, not the colour of the build. An answer on facts is a log of one particular decision and is kept next to that decision. And remember that flang run does not compute an unproved program at all without the --trust key.

13. разбор over yes and no instead of если

The habit from item 8 — “everything through разбор” — goes too far when the result of a comparison is matched.

модуль «Порог»

тотальная функция «Не ниже порога»
  принимает число: неотрицательное, порог: неотрицательное
  возвращает число
  обеспечивает «не ниже порога» результат не меньше порог
  пример «выше порога»
    дано число равно 7
    дано порог равно 5
    ожидается 7
  пример «ниже порога»
    дано число равно 3
    дано порог равно 5
    ожидается 5
  разбор (число не меньше порог)
    случай да
      то число
    случай нет
      то порог

What happens. The code works and the examples pass, but the promise «не ниже порога» (not below the threshold) stays сетка 2 значения, and flang check --proof exits with code 3. The proof kernel reduces the goal by the condition of an если; matching a flag on the cases да and нет breaks that rule.

The right way. Comparisons of numbers and strings go through если. The same code with если число не меньше порог то число иначе порог:

модуль «Порог»

тотальная функция «Не ниже порога»
  принимает число: неотрицательное, порог: неотрицательное
  возвращает число
  обеспечивает «не ниже порога» результат не меньше порог
  пример «выше порога»
    дано число равно 7
    дано порог равно 5
    ожидается 7
  пример «ниже порога»
    дано число равно 3
    дано порог равно 5
    ожидается 5
  если число не меньше порог
    то число
    иначе порог

a13bn.flang: ПРОВЕРЕНО САМОСТОЯТЕЛЬНО — утверждений 1: доказано 1, условно 0, сетка 0, объявлено, не доказано 0, отвергнуто 0, нарушено 0; законов на сетке 0, на веру 0 — код возврата 0

Keep разбор for the questions “what kind of value is this” and “is the list empty”.

14. An “obvious” promise on the type число

Task. The absolute value of a number is non-negative — what is there to check.

модуль «Модуль числа»

тотальная функция «Модуль»
  принимает х: число
  возвращает число
  обеспечивает «модуль неотрицателен» результат не меньше 0
  пример «минус три»
    дано х равно -3
    ожидается 3
  если х не меньше 0
    то х
    иначе 0 минус х

тотальная функция «Модуль не числа»
  возвращает число
  пример «ноль на ноль»
    ожидается 0
  «Модуль» от (0 делить на 0)

What happens.

FLANG_EXAMPLE: пример «ноль на ноль» функции «Модуль не числа»: FLANG_PROPERTY: нарушено свойство «модуль неотрицателен» функции «Модуль»

flang numbers are machine floating-point numbers (IEEE-754). 0 делить на 0 passes type checking and yields “not a number”; every comparison with it is false, and “the absolute value is not below zero” stops being true. For the same reason the если from item 13 with the type число instead of неотрицательное is not proved: the kernel keeps “not a number” in mind. Another trap of the same kind is negative zero: −0 and 0 differ when compared for equality.

The right way. Declare неотрицательное wherever a value is non-negative: this gives the kernel bounds, and half of the promises get proved by themselves. Count money in whole kopecks (the type сотых), and divide only where the divisor is certainly not zero.

Model boundaries

15. A giant module

Task. “Let’s describe the whole company in one model, so everything is in one place.”

The first thing such a model trips over is homonyms. An order in sales and an order in logistics are different things, and a second declaration with the same name is refused:

модуль «Компания»

объект «Заказ»
  «номер»: строка
  «сумма»: неотрицательное

объект «Заказ»
  «номер»: строка
  «вес»: неотрицательное

FLANG_TYPE в файле g1.flang, строка 7, столбец 1: тип «Заказ» объявлен дважды

Then a less obvious mechanism kicks in: a record in an example must set all fields of the object. An object with six fields, of which the rule reads one, gives five errors on every example:

модуль «Компания»

объект «Заказ»
  «номер»: строка
  «сумма»: неотрицательное
  «вес отправления»: неотрицательное
  «регион доставки»: строка
  «кредитный рейтинг»: неотрицательное
  «канал продаж»: строка

тотальная функция «Скидка»
  принимает заказ: «Заказ»
  возвращает число
  пример «большая покупка»
    дано заказ равно запись «Заказ» с «сумма» равным 20000
    ожидается 2000
  если заказ.«сумма» не меньше 10000
    то (заказ.«сумма» умножить на 10) делить на 100
    иначе 0

FLANG_TYPE в файле g2.flang, строка 14, столбец 3: пример «большая покупка»: аргумент «заказ»: не задано поле «номер» записи «Заказ»
FLANG_TYPE в файле g2.flang, строка 14, столбец 3: пример «большая покупка»: аргумент «заказ»: не задано поле «вес отправления» записи «Заказ»
FLANG_TYPE в файле g2.flang, строка 14, столбец 3: пример «большая покупка»: аргумент «заказ»: не задано поле «регион доставки» записи «Заказ»
FLANG_TYPE в файле g2.flang, строка 14, столбец 3: пример «большая покупка»: аргумент «заказ»: не задано поле «кредитный рейтинг» записи «Заказ»
FLANG_TYPE в файле g2.flang, строка 14, столбец 3: пример «большая покупка»: аргумент «заказ»: не задано поле «канал продаж» записи «Заказ»

This is not nitpicking but a gauge of coupling: the cost of an example grows with the size of the object, and a dumping-ground object makes examples unportable long before the model becomes hard to read.

The right way. A module is a bounded context: one language, one owner, one reason to change. A function takes only what takes part in its decision, and overlaps get their own objects with their own names.

16. String statuses instead of a type with variants

Task. “An order has a status, let’s compare it to a string — why bother with variants.”

модуль «Статус строкой»

объект «Заказ»
  «номер»: строка
  «статус»: строка

тотальная функция «Можно отгрузить»
  принимает заказ: «Заказ»
  возвращает признак
  заказ.«статус» равен "готов к отрузке"

What happens. The check is green, and even --proof answers with code 0 — the model claims nothing. The typo in "готов к отрузке" is an ordinary string literal; the compiler has nothing to compare it with. The function never answers да; with a live example you would see it, without one — never.

The right way. Everything transitions and permissions hang on is declared as a type with variants. The same typo in a variant:

модуль «Статус вариантом»

тип «Статус»
  вариант «Создан»
  вариант «Готов к отгрузке»

тотальная функция «Можно отгрузить»
  принимает статус: «Статус»
  возвращает признак
  разбор статус
    случай «Создан»
      то нет
    случай «Готов к отрузке»
      то да

FLANG_UNKNOWN_NAME: неизвестный вариант «Готов к отрузке»
FLANG_MATCH_NOT_EXHAUSTIVE в файле s2.flang, строка 10, столбец 3: разбор «Статус» не покрывает «Готов к отгрузке»

The typo is caught by the compiler, not by a warehouse operator. A string stays a string where it really is data: a number, a region, an address.

Practice in the sandbox

Add a function «Средний чек» (average receipt): if the amount is at least 1000, then 7 percent of the amount — and add it to the total in «Рассчитать скидку». Run the check. Six examples turn red: «обычная покупка» (an ordinary purchase) gets 350 instead of 0, and two large purchases give FLANG_PROPERTY: нарушено свойство «скидка ограничена» — items 7 and 9 of this catalog in a single move.

Add the field «курс валюты» является запросом to the object and find FLANG_UNKNOWN_NAME in the answer. Then declare it as «курс валюты»: число and make sure the check passes again.

Move the far-zone threshold from 500 to 600 kilometres so that one example stops passing. Then fit the ожидается line to the new result and state in one sentence what the model has stopped guaranteeing.

Find the two proved promises of the function «Можно отгрузить» in the report. Replace иначе нет in its body with иначе да and run the check again: both promises become сетка 2 значения, although the examples still pass. Explain why green examples guarantee nothing here.

Model code review checklist

1. Are there action verbs in the model — “send”, “charge”, “retry”? An action is described by a план, a decision by a function.
2. Is a function named after an accomplished fact instead of a permission or an obligation?
3. Does “today”, an exchange rate or a lot come into the model from inside? External things arrive as a field or an argument.
4. Can two rule functions contribute at the same time? Then it is addition, not choice — and the overlap needs an example.
5. Is there an если … иначе если chain over the kind of a value? You need разбор.
6. Is there a разбор over да and нет of a comparison? You need если.
7. Is every boundary covered by an example — a value exactly at the threshold, not near it?
8. Does the body clip the result to fit the promise? A proved promise that repeats the body checks nothing.
9. Does every promise have an example? Without one it is “declared, not proved”.
10. Does CI run flang check --proof, and is code 3 kept from counting as green?
11. Did an ожидается line change together with the rules without a link to a business decision?
12. Where can the type число be replaced with неотрицательное or сотых?
13. Does the function need every field of the object? Extra fields are paid for in every example.
14. Are there objects from another context in the module — by name, by owner, by reason to change?
15. Are statuses a type with variants rather than strings?

Catalog cases on this topic