flang компилятор доказывает, что программа не зациклится 0.6.2 GitHub English

Приложение в браузере

«Градины» — приложение во вкладке, целиком на flang. Не стенд: показывает состояние, отвечает на действия человека, считает.

Наберите число цифрами, нажмите «пуск» — и число падает по правилу Коллатца: чётное делится пополам, нечётное умножается на три и плюс один. «Шаг» двигает на такт, «бег» считает сам, пока не остановят.

sh web/sobrat.sh                                          # напечатать модуль в JavaScript
bootstrap/flang io web/stand.flang --max-orders 1000000   # поднять стенд
# открыть http://127.0.0.1:8908/

Ни Node, ни npm, ни python3 -m http.server: печатает модуль двоичный компилятор, отдаёт страницу стенд, написанный на flang (web/stand.flang).

Раньше сборки не было вовсе — страница ввозила flang/src/parser.mjs и разбирала hailstone.flang прямо во вкладке. Второй реализации языка в дереве больше нет, и вместе с ней у страницы пропали все три ввоза: приложение не открывалось никак. Теперь во вкладку едет напечатанный модуль — 61 453 байта против почти двух мегабайт компилятора.

Сколько чего написано

строкчтона чём
301web/app/hailstone.flang — всё приложениеflang
499web/stand.flang — стенд, отдающий страницуflang
397flang/src/emit/js/flang_host_browser.js — хозяин вкладкиJavaScript
241web/browser-probe.sh — прогон в настоящем браузереоболочка
88web/app/index.html — разметка; строк JavaScript в ней нольHTML

Строк JavaScript, написанных руками ради этой страницы, — ноль. Тег запуска несёт два признака и ни одного выражения:

<script type="module" src="../../flang/src/emit/js/flang_host_browser.js"
        данные-модуль="./gradiny.js"></script>

Хозяин вкладки — не «своё» приложения, а тело цели печати «js»: он один на все страницы дерева и обязан быть на языке цели, как flang/src/emit/c/*.c обязаны быть на C.

Из 301 строки flang 106 — примеры (пример, дано, ожидается), то есть треть файла это проверки, лежащие рядом с проверяемым. Функций 16, тотальных 16 из 16, примеров 31, упавших 0.

В хозяине без комментариев 158 строк. Прикладной логики в нём ноль: он не знает ни про Коллатца, ни про кнопки — он знает про места и события.

Толкающий цикл лёг на нынешний уклад. Правок в runPlan — ноль

Это главное измерение работы, и ответ вышел не тот, что ждали.

Цикл поручений тянущий: runPlan сам просит у программы следующее поручение. Браузер толкающий: события зовут программу. Оценка была «1 функция

одной строкой, написанной задолго до всякого браузера:

отклик = проверитьОтклик(await исполнить(поручение), поручение, план)

await и есть инверсия управления. Хозяин браузера возвращает обещание, которое разрешает addEventListener; пока план ждёт, стек пуст, вкладка жива и отзывчива, а разбудит план не программа, а человек либо часы. Прогон это подтверждает числом: «бег» довёл 27 до единицы за 111 тактов, каждый — пробуждение по часам, и «сброс» после них сработал сразу.

То есть тянущий цикл и толкающий мир — не противоположности. Тянущим цикл выглядит изнутри программы; снаружи он ровно столько же толкающий, сколько хозяин захочет.

Чего переворот всё-таки стоил — три вещи, все названные

1. Предел поручений — мера пакетной программы. DEFAULT_MAX_ORDERS равен 10 000, и для программы, которая кончается, это ловушка на зациклившуюся. Для вкладки то же число значит «приложение умрёт после пяти тысяч нажатий». Чинится вызывающим (maxOrders: Infinity в index.html), правки в io.mjs не потребовалось — но умолчание для приложения неверное, и это стоит помнить.

2. Журнал runPlan — течь, растущая со скоростью действий человека. журнал копит {поручение, отклик} на каждое поручение и не отдаётся никому до конца плана, которого у приложения нет. Один полёт числа 27 — это 225 записей за сорок секунд. Вкладка, открытая на час с включённым бегом, накопит их сотни тысяч. Это не починено: чинить надо в io.mjs, а всякая правка там тянет эталон, и делать её мимоходом нечестно. Названо числом, чтобы не забылось.

3. Машина продолжений ждёт РОВНО ОДНО. «Продолжение» несёт одно поле поручение, значит двух ожиданий сразу не выразить. А источников у приложения два: человек и часы. Поэтому они сведены в одно поручение — «Ждать событие» с срок равным 350 значит «разбуди на действии человека или через 350 мс, что раньше». Это не обход ограничения, а его правильное прочтение: выбор «что раньше» принадлежит хозяину, программа же называет оба условия сразу.

Чего в язык не втащено, и почему

Ни DOM, ни window, ни addEventListener, ни querySelector — ни в словаре (flang/src/io.mjs), ни в спецификации, ни в одной строке .flang. Программа называет место — строку "экран", которую придумала сама, — и не знает, куда хозяин это место положит. Граница та же, что между путь и файловым дескриптором.

Поручение несёт ТЕКСТ, а не разметку. Это сознательный отказ, и вот его цена. Чтобы программа могла описывать вид (списки, таблицы, вложенность), словарю нужна четвёртая сумма — дерево разметки, — а поля встроенных сумм сегодня плоские: string, number, any. Рекурсивный именованный тип внутри встроенной суммы пришлось бы повторить в эталоне и в восьми целях печати. Поэтому вид рисует хозяин, а программа отдаёт ему текст; innerHTML в хозяине нет и не будет — разрешить разметку значило бы втащить в словарь второй язык, на котором программа не писана и который никто не проверяет. Тот же довод и с теми же числами стоит у сокращателя ссылок, и это не совпадение: у обоих приложений один хозяин.

Тотальность цела. Задача выбрана ровно за это: «Шаг градины» — тотальная функция, а завершается ли последовательность, не доказано никем в мире. И язык этого не требует: ни одна функция не повторяет шаг, повторяет его человек либо часы. Незавершаемость живёт в цикле хозяина — там же, где у службы, — а обработчик события оказался ровно таким же тотальным шагом, каким уже был обработчик запроса.

Чем проверено без рук

Двумя прогонами, и второй нашёл то, что первый пропустил.

flang/test/host-browser.test.mjs — без браузера. Подставной документ: объект с querySelector, querySelectorAll и addEventListener, тридцать строк. Настоящий хозяин работает с ним так же, как с окном вкладки — тот же приём, каким nodeHost проверяется без сети. Шесть проверок, среди них «часы будят план сами» (6 → 1 за 8 шагов без единого нажатия) и «нажатия, случившиеся пока план считал, не теряются».

web/browser-probe.sh — в настоящем браузере, без Node и без npm. Playwright берётся из окружения, в зависимости flang не входит. Шесть сверок экрана, все побайтовые.

Второй прогон нашёл беду, невидимую первому: у кнопки в HTML есть свойство value, и оно пустая строка. Хозяин спрашивал его раньше объявленного данные-значение и получал от всякого нажатия пустоту — в браузере приложение отвечало «непонятная клавиша «»» на каждую цифру, было 1 сверка из 6. Подставная страница этого не ловила, потому что value у неё не было вовсе. Починены оба: и хозяин, и проверка. Мутация подтверждена — со старым порядком падает 3 проверки из 6.

Что осталось из семи пунктов разрыва

Закрыто 5 из 7: поручения экрана (+2 вместо +4), отклики экрана (+3), хозяин браузера (250 строк), цикл событий (0 правок), согласование (6 файлов вместо 7 — их и оказалось шесть).

Не закрыто 2: