Песочница

Здесь flang проверяет текст прямо во вкладке: силлогизм, записанный словами, или программу на flang с утверждениями, теоремами и постусловиями. Компилятор с ядром доказательств собран в WebAssembly и работает в браузере; на сервер не уходит ничего, и ссылка «Поделиться» несёт текст в адресе после #, который браузер серверу не отправляет.

Песочнице нужен JavaScript и браузер с WebAssembly. Без них те же проверки делает
двоичный компилятор: flang check файл.flang --proof.

Что во что превращается

Песочница сама решает, что перед ней, по первому слову текста.

Текст начинается с модуль или категория — это программа на flang. Её проверяет flang check --proof и печатает ведомость доказательства, как в терминале.
Любой другой текст — рассуждение по-русски: словарь (Понятие:, Свойство:, Имя:), посылки и заключение после слова «Следовательно». Переводчик flang/proof/probes/syllogism/sentences/translator.flang строит из него программу, ядро судит её с --proof --strict, и ответ звучит словами судьи: «СЛЕДУЕТ» или «НЕ СЛЕДУЕТ» с примером против.

После проверки ядра песочница отдаёт запись доказательства сверщику (flang/proof/checker/checker.c), собранному отдельным модулем WebAssembly, и печатает его ответ следом. Утверждение, которое сверщик проиграл заново, стоит не только на слове ядра.

Примеры

Силлогизм Barbara: заключение выводится из посылок.

Понятие: человек, люди.
Понятие: грек, греки.
Свойство: смертен, смертны.

Все люди смертны. Все греки — люди. Следовательно, все греки смертны.

Утверждение следствия: из «все люди смертны» и «Сократ смертен» не следует, что Сократ — человек. Ядро не выводит цель, судья называет пример против.

Понятие: человек, люди.
Свойство: смертен, смертны.
Имя: Сократ.

Все люди смертны. Сократ смертен. Следовательно, Сократ — человек.

Утверждение о своём типе, доказанное индукцией.

модуль «Своё натуральное»

тип «Нат»
  вариант «Ноль»
  вариант «Следующий» содержит пред: «Нат»

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

утверждение «шаг растит счёт на один»
  для всех н: «Нат»
  утверждаем («К числу» от (вариант «Следующий» с пред равным н)) равно ((«К числу» от н) плюс 1)

теорема «шаг растит счёт на один»
  дано н: «Нат»
  утверждаем («К числу» от (вариант «Следующий» с пред равным н)) равно ((«К числу» от н) плюс 1)
  индукция по н
    случай вариант «Следующий» с пред как п
      то по предположению
  следовательно доказано

Функция с постусловием: обещание обеспечивает доказывается для всех входов.

модуль «Привет»

тотальная функция «Удвоить»
  принимает н: неотрицательное
  возвращает число
  обеспечивает «удвоенное не меньше исходного» результат не меньше н
  пример «дважды два»
    дано н равно 2
    ожидается 4
  н плюс н

Ложное утверждение: при н = 0 удвоение не больше исходного. Ведомость говорит «объявлено, не доказано», итог — «НЕ ПРОВЕРЕНО» с кодом 3.

модуль «Ложное»

утверждение «удвоение всегда больше»
  для всех н: неотрицательное
  утверждаем (н плюс н) больше н

У блоков программ на flang на других страницах документации стоит ссылка «запустить в песочнице»: она открывает эту страницу с текстом блока в адресе.

Как это устроено

что	где	чем собрано
компилятор с ядром	`playground/flang.wasm`	`bootstrap/*.c`, `clang --target=wasm32-wasi`
сверщик	`playground/checker.wasm`	`flang/proof/checker/checker.c`, тем же `clang`
переводчик рассуждений	`playground/reasoning.js`	`bootstrap/flang emit --target js`
библиотека	`playground/library.tar`	`flang/stdlib/.flang` и `flang/core/.flang`
хозяин WASI и песочница	`playground/flang_host_browser.js`	`flang/src/emit/js/flang_host_browser.js`

Все пять файлов собирает шаг сборки сайта (bootstrap/flang run-script playground:build); в дереве их нет. Хозяин WASI держит файловую систему в памяти вкладки: исходник пользователя, библиотеку (её песочница скачивает, только если в тексте есть использует) и временный каталог /tmp. Компилятор и сверщик работают в отдельном потоке (Web Worker), страница при этом не замирает.

Тот же хозяин работает и под Node, без браузера:

node flang/src/emit/js/flang_host_browser.js docs/site/out/playground "$(cat текст.txt)"

Код возврата у него тот же, что у проверки: 0 — следует или доказано, 1 — не следует, 3 — не доказано.

Этим путём сборка сайта и пробует песочницу (bootstrap/flang run-script playground:probe, план scripts/site/playground-probe.fscript): Barbara обязана «следовать», и сверщик обязан сойтись с записью; утверждение следствия — «НЕ СЛЕДУЕТ» с кодом 1; ложное утверждение — «НЕ ПРОВЕРЕНО» с кодом 3 и ни одного «ДОКАЗАНО».

Чего в песочнице нет

Процессов. В WebAssembly нет fork и exec, поэтому компилятор не может сам позвать сверщика и пишет «НЕЗАВИСИМО НЕ ПРОВЕРЕНО этим модулем»; сверщика зовёт хозяин следом, вторым модулем.
Сети и файлов машины. Сокетов нет, файлы — только в памяти вкладки.
Сверки ввозов. Программе с использует сверщику нужны записи ввезённых модулей (--зависимость); песочница их не строит, и сверщик отвечает кодом 1.
64-битного адреса. Модуль собран под wasm32: памяти не больше 4 ГиБ, а вшитый предел шагов 8·10¹² в 32-битный size_t не влезает и становится 2 770 894 848 — об этом при сборке предупреждает clang.