Оракулу законов мешала тотальность, а не отсутствие функций первого класса

Тринадцать файлов на JavaScript (3 874 строки) держались в рабочем пути одним доводом, записанным в трёх местах дерева: «законам мало разобрать программу, надо её ВЫПОЛНИТЬ, а передать вычислитель функцией в flang нечем — функций первого класса у языка нет». Довод неверен. Вычислитель не надо никуда передавать: он зовётся по имени, как любой другой модуль. Мешало другое — обещание тотальности.

Чем подтверждено. Проба в два прогона, ветка work/zakony-na-flang (605cd5ca):

тотальная функция «Проба тотальная»
  ...
  «Вызвать» от «программа» и «имя» и «аргументы» и 1000000 и 10000

отвергается: FLANG_NOT_TOTAL — «тотальная функция «Проба тотальная» вызывает обычную функцию «Вызвать»: обычная функция может не завершиться». Та же функция без слова «тотальная» — valid: true, диагностик 0.

Причина в том, что в flang/self/interpret.flang 49 функций из 280 объявлены обычными, и обе точки входа вычислителя («Подготовить программу», «Вызвать готовое») среди них. Иначе и быть не может: вычислитель исполняет произвольную программу, а её завершение неразрешимо. Предел витков и предел глубины стоят на ней при работе, но статически это ничего не доказывает.

Звать вычислитель по имени язык умел всё это время, и в дереве уже был пример — flang/self/proof-kernel.flang ввозит «Вычислитель flang» из "interpret.flang" с 16 августа. Довод про первый класс никто не проверял прогоном; он был записан и трижды переписан из места в место.

Чем ограничено. Тотальность не «обходится» — она платится: у перенесённого оракула (flang/self/oracle.flang, 441 строка) 23 функции из 42 обещания тотальности не несут. Это честная цена, а не поблажка: оракул выполняет чужую программу. У самих пяти законов рядом обычных функций по-прежнему ноль — граница проходит ровно по вызову вычислителя и не размазана по слою.

Что это стоило и что дало. Оракул пяти объявленных свойств перенесён в дерево и сверен с прежним побайтово: 274 программы корпуса (4 непустые таблицы, 706 строк) и 48 нарочных программ проверки (39 непустых, 1169 строк) — расхождений 0. Пять законов переключены в рабочем пути: 961 строка JavaScript ушла из пути целиком, заплачено 234 строками JavaScript и 441 строкой flang.

Урок шире одного файла. Довод «язык этого не умеет» стоит проверять прогоном раньше, чем переписывать его в четвёртое место. Здесь он держал тринадцать файлов больше недели и стоил одной пробы в шесть строк.

Связано: checks-that-stopped-comparing, the-second-implementation-cannot-be-replaced