Самораскрутка меряется четырьмя кусками JavaScript, три закрыты
Компилятор flang пишется на самом flang; свидетель на JavaScript нужен, пока эталон его не догнал. Состояние на 15 августа 2026:
| Кусок | Было | Стало |
|---|---|---|
| Ядро доказательств | 1020 расхождений из 7888 | 15 828 сверок, 0 расхождений |
| Интерпретатор | 2240 из 2317, 77 форм вне среза | 2318 из 2318 |
| Вычисления для законов | 0 из 4480 своим языком | 4480 из 4480 |
| Связка поверхность↔ядро | 1281 строка | в работе |
Четвёртый кусок — flang/src/obligations.mjs (301 строка; было 373, пока в нём лежали какНаписан и одинаковы — они выехали в flang/src/as-written.mjs) и flang/src/proofterm.mjs (938). Всё, что они вызывают, на flang уже написано; не перенесена сама связка. Пока она на JavaScript, свидетель выбросить нельзя.
Цена оказалась вчетверо меньше опасений. Предупреждали, что один шаг компилятора на flang стоит 1500–3000 шагов свидетеля и всё упрётся в скорость. По факту: +27 % по часам, с 32,6 до 41,5 секунды.
Состояние дерева на 16 августа 2026: main обновлён (8203f39 → 6e186c5, 402 коммита), семь целей печати из восьми теперь на flang, веток осталось 39 из 212.
Важная деталь про честность. Запасной путь к свидетелю убран из кода вовсе, а не оставлен на всякий случай — иначе он тихо срабатывал бы и никто бы не заметил. Ср. checks-that-stopped-comparing.
Связано: byte-for-byte-comparison, what-is-deferred