Proofs: theorems, proof records and scientific boundaries

This is the most delicate chapter of the course. The word “proved” in flang means a narrow and checkable thing: a function’s promise (обеспечивает) holds on all inputs of its types, and the proof kernel derived this using rules from a closed list. It does not establish the truth of a business rule. The statement “the compiler proved that the order may be shipped” is wrong. The right one: “it is proved that the admission function answers “no” on any unpaid order; on this order’s data it answered “yes””.

Minimal example (theorem)

модуль «Баллы лояльности»

тотальная функция «Баллы за стаж»
  принимает лет: неотрицательное
  возвращает число
  для всех лет обеспечивает «баллы не отрицательны» результат не меньше 0
  пример «новый клиент»
    дано лет равно 0
    ожидается 0
  пример «три года»
    дано лет равно 3
    ожидается 30
  если лет не больше 0
    то 0
    иначе 10 плюс («Баллы за стаж» от (лет минус 1))

теорема «баллы не отрицательны»
  дано лет: неотрицательное
  утверждаем результат не меньше 0
  индукция по лет убывает лет
    случай 0
      то по примеру «новый клиент»
    случай любое
      то по предположению
  следовательно доказано

The line для всех лет обеспечивает is a promise about any length of membership, not about the written examples. The theorem bears the name of the promise it proves and runs induction on лет (years): the base case is closed by the example “new customer”, the step by the induction hypothesis.

What the compiler does

flang check --proof judges every promise and says what carries it:

  постусловие «баллы не отрицательны» функции «Баллы за стаж» — доказано индукцией по «неотрицательное»: база 1 случай, шаг при допущении на убывшем «лет» (1 случай), правила сведения: неотрицательность по построению — утверждение обо ВСЕХ значениях отрезка «неотрицательное» [0, 9007199254740991], а не о написанных: отрезок конечен, спуск строг и дна не проскакивает

The kernel checks every step of a theorem instead of taking it on trust. A wrong step is a refusal. If the induction step is closed with an example instead of the hypothesis:

FLANG_PROOF_INDUCTION_STEP в файле loyalty-points.flang, строка 24, столбец 10: шаг 1, шаг «спуск» теоремы «баллы не отрицательны»: в заключении случая «спуск» свободны «лет», поэтому значений у него бесконечно много, а пример — одно. …

Often a theorem is not needed at all: for this function the kernel derives the same promise without it. The order of work is always the same: first обеспечивает, then flang check --proof, and only if the promise stays unproved — a theorem.

Promise, verdict and kernel rule

Every promise in the report gets one of the verdicts, and they are not interchangeable:

The kernel does not search for a proof: it applies rules from a closed table and names the one that worked — “case split on the inner condition of the goal”, “order by construction”, “non-negativity by construction”. Hence the boundary. The promise “the discount is at most 15,000” over a sum of percentages is not derived by the kernel, and in the report it stays on examples:

  постусловие «скидка ограничена» функции «Рассчитать скидку» — сетка 5 значений (примеры функции): нарушений НЕ ИСКАЛИ — прогона примеров не было, посчитано только их число. Это не доказательство — теоремы при утверждении нет

Such a promise does not vanish: it is checked on every call of the printed program, and flang run will not compute such a program without explicit consent:

не доказано: утверждений 4: доказано 1, сетка 3, на веру 0 — запуск только по явному согласию: --на-веру

Consent is given with the --trust key for one run. The report has a section “принято на веру” (taken on trust) — what the program asks you to accept without a check. In the course models it is empty.

Morphisms and composition

An allowed transition “if A, then B is allowed” is a function with an implication promise in flang. The kernel derives a chain of transitions on its own by unfolding the call. In the model credit-limit.flang the function “the limit may be set” calls “risk check allowed”, and the promise “no scoring, no limit” is proved without a theorem:

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

One function’s promise can also rest on another’s explicitly — through a theorem with a по свойству «имя» (by property) step. The kernel accepts such a step only if the conclusion contains a call of the function whose promise is named: the promise is instantiated at the call site, and the kernel does not invent call sites.

For readers coming from category theory, the language also has a categorical surface: морфизм «имя» из «А» в «Б» даёт «Функция», единица, a категория with its own equality, функтор, a закон attached to an arrow:

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

тип «Состояние заказа»
  вариант «Собран»
  вариант «Отгружен»

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

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

морфизм «отгрузить» из «Состояние заказа» в «Состояние заказа»
  даёт «Отгрузить собранный»
  закон «отгруженный заказ повторно не меняется»
    пример «повторная отгрузка»
      дано стадия равно вариант «Отгружен»
      ожидается вариант «Отгружен»

единица «Состояние заказа»

категория «Исполнение заказа»
  морфизм «отгрузить»
  объект «Состояние заказа» даёт «Стадии равны»

The category laws — that equality is an equivalence, that composition respects it and is associative — are not proved by the compiler but counted on a finite set of values:

категория «Исполнение заказа»: сетка 2 значений на 1 объектах, троек стрелок 2, нарушений 0 — ПОСЧИТАНО НА СЕТКЕ, не доказано

The report exits with code 3. Without a declared equality (объект «…» даёт «…») the laws are not counted at all, and the check answers with code 2 — “checked NOT TO THE END”. Monoids, monads, functors and isomorphisms are named in the report one by one, but their laws are likewise judged only on a grid or not judged at all. Business rules do not need the categorical surface: admissions and transitions are written as functions, and there the promises are proved.

Deriving on data

A proof speaks about a function, not about a particular order. The question “may ЗК-7781 be shipped” is answered by another command — flang facts: it evaluates a claim on JSON facts and returns a verdict with steps (details in chapter 10). This is evaluation, not proof: true for this snapshot and only for it.

The two answers connect like this. Proved: the function “may be shipped” answers “no” on any unpaid order. Computed: on these facts it answered “yes”. Together: the order in these facts is paid and confirmed by the warehouse — to the extent that the facts are true.

What is missing here. The verdict of flang facts carries no fingerprint of the data snapshot and no timestamp — it is a plain JSON answer. If the decision has to be kept for an audit, store the fact snapshot, the program text and the whole answer together with it; the SHA-256 fingerprint of the snapshot you have to compute yourself.

The proof record and the checker

flang check --proof --record <файл> writes a proof record — a text file listing, for every promise, its verdict, the theorem and each of its steps with the source line:

запись доказательства 1
исходник loyalty-points.flang
строк 26
знаков 633
отпечаток 532072833 565577387
ядро 2
утверждений 1
отпечаток256 9a191b6a56db5101c64773a532990a67d755be6bcc018f2ee3a3f5d0c6ef673f

утверждение «баллы не отрицательны» функции «Баллы за стаж» строка 6
  вид postcondition
  для всех «лет» строка 6
  вердикт доказано
  теорема «баллы не отрицательны» строка 17
  …
    шаг 1 строка 24 закрывающий по предположению
  следовательно доказано да

The record is re-checked by a separate program written in C — the checker. It has never seen the compiler: it reads the source and the record, compares the fingerprints and replays every proved step anew. On an honest record:

  утверждение «баллы не отрицательны»: ПРОВЕРЕНО (на слово ядра: посылок и утверждений 0, шагов 0)

Now swap one step in the record — “by hypothesis” for “by example «три года»”:

НЕ СОШЛОСЬ: теорема «баллы не отрицательны», строка 24: запись говорит «по примеру «три года»», а в исходнике написано «по предположению»

Change the source after recording (10 плюс to 20 плюс) and give the checker the old record:

НЕ СОШЛОСЬ: первый отпечаток не сошёлся — запись не от этой программы; второй отпечаток не сошёлся — запись не от этой программы; отпечаток256 записи «9a191b6a56db5101c64773a532990a67d755be6bcc018f2ee3a3f5d0…

Where the checker is available. In the sandbox at /flang/ it runs after every check — you can see it in the answer. The flang binary from install.sh does not include it: flang check --proof says the proved claims “rest on the kernel’s word” and suggests building the checker from the language sources (make -C flang/proof/checker) and naming it in the FLANG_CHECKER variable.

What the record lacks compared with the usual “certificates”: a signature, a timestamp and the data. The record is bound to the program text by a SHA-256 fingerprint and speaks only about the program.

What this does NOT prove

• The truth of the business rule. “Only a paid order may be shipped” is a business decision. The kernel proves that the function keeps it, not that the rule is right.
• The correctness of the promise. Proved is not the same as right. A promise that repeats the function body is proved for free and means nothing; a promise with a mistake in it is proved just as easily as one without.
• The completeness of the model. The admission function knows nothing about sanctions lists or a blocked customer. A correct conclusion from an incomplete model is still a correct conclusion from an incomplete model.
• The freshness of the snapshot. The verdict of flang facts holds for the facts at the moment of the call. The world may change between the verdict and the shipment.
• The printed program. The proof is tied to flang check. Nobody checks that the code from flang emit (C, Go, JavaScript and the rest) matches the source; the flang run evaluator is not proved either.
• Numbers as in mathematics. The language’s numbers are IEEE-754: 0 делить на 0 gives “not a number”, and the promise “an absolute value is never below zero” is false on it. The type неотрицательное is the segment [0, 2⁵³−1], and only it gives the kernel bounds.
• Time, side effects and concurrency. Claims like “after payment the order will not become a draft” cannot be expressed in the language: the kernel has no temporal logic.

A separate note on the scientific and patent status. The fact that the kernel applies a closed list of rules while an independent program re-checks the record is a good subject for research and machine-checkable evidence. For a publication it is not enough: you need a formal semantics, inference rules in the form of judgments, proofs of the chosen soundness properties, a reference implementation, a replication package and measurements.

For a patent the situation is stricter. Neither the Curry–Howard correspondence, nor induction, nor static typing, nor a cryptographic hash, nor proof-carrying code, nor tool calls by agents can be claimed as new. What may be protectable is a specific combination of features and a technical result, and a conclusion about novelty is only allowed after a patent and bibliographic search. Public disclosure before filing destroys novelty in a number of jurisdictions, so the order is: prior-art search, consultation with a patent attorney, filing, publication.

Practice in the sandbox

Transitions proved without a theorem:

Replace the body of “the limit may be set” with заявка.«риски одобрили» and see which promises drop to a “grid”: without the call to “risk check allowed” the kernel has nothing to derive the scoring claims from.

The shipping admission and the functions the flang facts verdict rests on:

A model where some promises rest on examples only:

In the sandbox the checker runs after every check — find its line “ПРОВЕРЕНО — запись сошлась с исходником” (checked — the record matches the source) in the answer.

Common mistakes

• FLANG_PROOF_INDUCTION_STEP — an induction step is closed with the wrong thing: an example where a name is still free, or the hypothesis in the base case.
• FLANG_PROOF_STEP — a theorem step does not follow. In the refusal the kernel lists what it can derive at this point — that shows what was missing.
• FLANG_PROPERTY — an example broke a promise. This is not “not proved” but a falsehood found on a concrete input.
• “grid N” read as “proved”. flang check without --proof exits with code 0 and says nothing about provability; with --proof a grid gives code 3.
• “COUNTED ON A GRID” for a category or a functor read as “the law is checked”. It is a check on a few values, and the report says so in words.
• A proof record kept without the source. The checker needs both files; an edited source will not accept the old record.

Checklist

1. Every promise a decision rests on reads “proved” in the report, not “grid”.
2. A theorem is written only where the kernel did not close the promise on its own.
3. CI runs flang check --proof, and code 3 counts as red wherever provability is required.
4. The “taken on trust” section has been read; a program that asks for trust needs a separate decision.
5. For a decision about an action the source, the proof record, the fact snapshot and the flang facts verdict are stored — otherwise the check cannot be repeated.
6. The proof record has been re-checked by the checker — in the sandbox or with one built from the language sources.
7. For the customer, instead of “it is proved that the order may be shipped”, say “it is proved that the admission rule holds on any order; on this data it allowed the shipment”.

Catalogue cases on this topic

Next: integration with any language