Capstone: order execution from model to service and form

The capstone puts everything from the course into one project: a domain object, a type of states, a calculation function with examples and a promise, shipping approval, an HTTP service, a form and TypeScript for CI. The rule is written once — in flang — and five parts of the system use it. Every step below shows the command and its real output.

1. The model

The model lives in static/spec/models/order-fulfilment.flang:

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

тип «Состояние заказа»
  вариант «Создан»
  вариант «Оплачен»
  вариант «Собран»

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

тип «Решение по отгрузке»
  вариант «Разрешено»
  вариант «Отказано» содержит причина: строка

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

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

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

тотальная функция «Допуск отгрузки»
  принимает заказ: «Заказ»
  возвращает «Решение по отгрузке»
  пример «склад не подтвердил — причина названа»
    дано заказ равно запись «Заказ» с «номер» равным "ЗК-7781" и «сумма» равным 20000 и «оплачен» равным да и «склад подтвердил» равным нет
    ожидается вариант «Отказано» с причина равным "склад не подтвердил заказ"
  разбор «Состояние» от заказ
    случай «Собран»
      то вариант «Разрешено»
    случай «Оплачен»
      то вариант «Отказано» с причина равным "склад не подтвердил заказ"
    случай «Создан»
      то вариант «Отказано» с причина равным "заказ не оплачен"

What is what:

• объект «Заказ» is the data a request arrives with: the number, the amount and two facts — whether the order is paid and whether the warehouse confirmed it.
• тип «Состояние заказа» holds three states. A value of this type cannot simply be read: it is taken apart with разбор, and the compiler requires all three variants to be named.
• «Скидка» computes money. Its examples are domain tests that run on every check.
• «Можно отгрузить» and «Допуск отгрузки» describe the allowed transition “assembled → may ship”. The first answers yes or no, the second returns a decision with the reason for a refusal.

None of this writes to a database or calls the courier service: the model only computes and decides.

The discount cap is stated in two ways. The branch если заказ.«сумма» больше 100000 то 10000 holds it, and the promise обеспечивает «скидка ограничена» результат не больше 10000 declares it. The second example shows that the cap is reached exactly: a promise that no example ever reaches checks nothing. Boundary traps are covered in the chapter on anti-patterns.

In the course’s working projects this model is split in two: the discount calculation lives in order-discount.flang (the HTTP service computes it), and shipping approval in order-shipment.flang (shipment-guard computes it). They are built the same way.

2. Architecture

The model is checked once, and independent branches grow from it. The form takes its fields from flang ast, the service computes the discount with a function printed by flang emit, the guard asks flang facts, CI compares the printed TypeScript, and an agent gets the same checks through flang --mcp-mode. When the rule changes, only the left node of the graph changes — the rest is rebuilt from it instead of being edited one by one.

3. Step by step

3.1 Checking the model

flang check static/spec/models/order-fulfilment.flang

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

The compiler parsed the program, inferred the types, proved that all four functions terminate, and ran the examples. This command says nothing about whether the promises are proved — the --proof flag shows that:

flang check static/spec/models/order-fulfilment.flang --proof

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

Both shipping promises are proved for any order, not just for the three written ones. The discount cap is not proved: the kernel does not derive the estimate “ten percent of the amount is at most ten thousand”, so the promise rests on three examples — that is what “сетка 3” means. Exit code 3 says so out loud. What to do about it is the team’s decision: either accept the grid and watch code 3 in CI separately, or rewrite the body so the bound matches an если branch.

The domain examples as a separate command:

flang test static/spec/models/order-fulfilment.flang

order-fulfilment.flang: примеров 6, прошло 6, не прошло 0

If the discount rule is ever changed to 12 percent, this step fails first — before the HTTP service and before the form.

3.2 Shipping approval from facts

Permission to ship is not a database field but the answer of flang facts on a data snapshot. The snapshot is plain JSON the service builds from its tables before deciding (static/spec/models/order-fulfilment.facts.json):

{
  "заказ": {
    "номер": "ЗК-7781",
    "сумма": 20000,
    "оплачен": true,
    "склад подтвердил": true
  }
}

flang facts static/spec/models/order-fulfilment.flang \
  --facts static/spec/models/order-fulfilment.facts.json \
  --claims '["«Можно отгрузить» от заказ равно да"]' --pretty

"claim": "«Можно отгрузить» от заказ равно да",
"holds": true,
"why": "«Можно отгрузить» от факта «заказ» = да; требование «равно да» выполнено",
"status": "verified"

The verdict comes with its steps: which fact was taken, which function was called, what it returned and what it was compared with. Only a function with proven termination can be called — flang facts refuses a non-total one before computing anything.

examples/spec/shipment-guard/guard.mjs wraps the same thing into a function for the service. It works with the model order-shipment.flang, where the order is looked up in a table by its number:

node examples/spec/shipment-guard/guard.mjs ЗК-7781

returns "allowed": true and exit code 0. The same number, but a snapshot in which the warehouse has not confirmed receipt:

node examples/spec/shipment-guard/guard.mjs ЗК-7781 --blocked

"allowed": false,
"why": "«Заказ с номером отгружается» от факта «заказы», факта «номер» = нет, а утверждение требует «равно да». Исходные факты — «заказы»: [{\"номер\":\"ЗК-7781\",\"клиент\":\"ООО Маяк\",\"оплачен\":true,\"склад подтвердил\":false}]; «номер»: «ЗК-7781»"

The model, the claim and the guard code did not change — only the snapshot did, and the decision changed with it. Exit code 1 makes the difference usable in a shell script and in CI. The real call to shipping.createShipment(orderId) comes strictly after allowed === true: the action lives outside the model, not inside the guard.

3.3 HTTP service

npm run spec:api

At startup the service runs flang test on order-discount.flang: if an example does not match, the process does not come up at all. Then the model is printed to JavaScript (flang emit --target js), and requests are computed by the printed function, with no compiler at runtime. Once started:

curl -s localhost:8788/discount -d '{"сумма":20000,"постоянный клиент":true}'
# {"discount": 3000}

curl -s localhost:8788/contract
# {"function": "Рассчитать скидку", "input": [{"name": "сумма", "type": "неотрицательное"},
#  {"name": "постоянный клиент", "type": "признак"}], "output": "number"}

/contract does not hardcode the list of fields — it takes them from flang ast. Add a field to the model and the contract updates itself. A request with the wrong input type (a string instead of a number) gets 400 with the reason, not 500:

{"error": "вход не подходит к «Покупке»: «сумма»: ждали неотрицательное целое", "code": "INPUT"}

3.4 Form

The form schema is a pure function of flang ast:

node examples/spec/form-schema/schema.mjs Покупка

{
  "id": "Продажи.Покупка",
  "title": "Покупка",
  "fields": [
    { "name": "сумма", "label": "сумма", "type": "неотрицательное", "control": "number", "required": true, "min": 0 },
    { "name": "постоянный клиент", "label": "постоянный клиент", "type": "flag", "control": "checkbox", "required": true }
  ]
}

examples/spec/react-form/DiscountForm.jsx draws a field for every element of fields, and pre-computes the discount in the browser with the same printed function «Рассчитать скидку». The user sees the discount without a request to the server, and the server still recomputes it on submit: the browser is not trusted, but nobody has to wait for it either. A broken model promise reaches the form as an error with code FLANG_PROPERTY — an answer of the form, not a UI crash.

3.5 Generating TypeScript

node examples/spec/typescript-codegen/generate.mjs
node examples/spec/typescript-codegen/generate.mjs --check

The first call runs the model’s examples and prints into generated/ the module program.ts, with its runtime next to it. The second writes nothing — it only compares. If someone edits the printed .ts by hand, --check names the stale files and exits with code 1. The detailed walkthrough is in the chapter on generation and CI.

3.6 CI

npm run spec:check
npm run spec:examples

The first command runs every program from the course chapters and all the models through the compiler; the second runs the tests of the working projects: the service, the guard, the form, generation and migration. The ready-made workflow examples/spec/ci/flang-check.yml installs flang and runs the steps in order: model check, examples, comparison of the printed code, integration tests. The cheapest step fails first, the most expensive one last. It is the same order as in steps 3.1–3.5.

4. Definition of done

• flang check passes and flang test passes;
• flang check --proof has been read: every promise is called “proved”, “grid N” or “declared, not proved”, and the team knows which ones rest on examples only;
• the discount cap promise is reached exactly by at least one example — otherwise it checks nothing;
• the form reads its fields from flang ast, not from a second list in the code;
• the service prints the model once at startup, not on every request;
• the guard requires allowed: true before the action is called;
• the external courier call is not inside the model;
• CI catches manual edits of the printed code with --check;
• the README lists which state transitions are allowed and why.

5. Typical capstone mistakes

• Hardcoding the form’s field list instead of reading flang ast — then the form and the model diverge with the very first new field.
• Calling shipping.createShipment without checking decision.allowed — the guard is pointless if nobody reads its answer.
• Committing the printed .ts without a --check step in CI — an edit that bypasses the model goes unnoticed until production.
• Accepting HTTP input without checking types — wrong input must come back to the client as 400, not surface as 500.
• Reading code 3 as “all good”. flang check --proof with code 3 means some promises were checked on examples only; flang run refuses such a program without --trust.
• Building the claim text from user input. The order number goes into the facts as data, not into the --claims text; the guard does exactly that.

6. Assignment by role

A junior adds a field to объект «Заказ» and checks that the form got a control without touching the JSX, and that an optional field (иногда является) became optional. A middle builds the Node endpoint and returns input errors as 400, not 500. A senior designs the data snapshot for flang facts and the transaction boundary around the guard — where the model’s responsibility ends and the optimistic lock begins. A lead checks that the names in the model match the language of the domain expert and decides which grid-backed promises the team accepts. An agent may propose a new example, but it has to pass flang check --proof and flang test before the proposal reaches a pull request.

Sandbox practice

1. Change the second example to an amount of 99999 and an expectation of 9999.9 — the check passes, but the discount cap is no longer reached by any example. Put the example back.
2. Delete случай «Создан» in «Допуск отгрузки» and read FLANG_MATCH_NOT_EXHAUSTIVE.
3. Add a variant «Отгружен» to тип «Состояние заказа» and see how many matches the compiler asks you to complete.

Maturity criterion

The project is done not when the model looks nice but when real duplication is gone: one model drives both the calculation and the test, and the adapters read flang ast and the printed code. Actions, the interface and the infrastructure stay in their own layers — the model replaces neither the repository, nor the event bus, nor React.

Go back to the catalog of applied cases, pick the one closest to your work and repeat the capstone in your own domain: one object, one function with examples and a promise, one approval function and one adapter (HTTP, form or CLI) that does not drag side effects into the model.

Where next: what begins beyond the specification boundary

The model in this course is a small part of flang. The language can do more than rules need: lists (отобразить, отфильтровать, свёртка), recursion with proven termination, strings, your own types with variants and a plan of actions with files, processes and the network (план, flang io). So the tooling around a rule — a parser for your own format, report assembly, CSV validation — can be written in the same language, not just the rule itself.

The boundary has another side too, and it is worth knowing in advance. The language’s logic has no state over time: the claim “after payment an order can never become a draft” cannot be expressed. There are no proofs about side effects: a plan describes an action, the environment executes it, and the kernel says nothing about the outside world. Processes exist, but claims about races and deadlocks do not. Neither flang run nor the printed code is itself proved: the proof is tied to flang check.

Any model prints to ten languages — C, C++, C#, Elixir, Go, Java, JavaScript, TypeScript, Python, Rust — with a single flang emit command (chapter «From Python, Go and shell»).

If you want to understand how the language itself works — how termination is proved, what the proof kernel can do and where its limits are — that is a separate track: «flang».

Catalog cases on this topic