Вторую независимую реализацию возместить нечем — её можно только сохранить в проверках
Компилятор, собравший сам себя байт в байт, доказал ровно одно: он согласован с собой. Про правильность это не говорит ничего. Компилятор с устойчивой ошибкой воспроизведёт её идеально и не заметит — это ловушка Кена Томпсона («Reflections on Trusting Trust», 1984). Ловит такое единственная вещь: вторая реализация, написанная порознь по той же спецификации.
Поэтому решение убрать реализацию на JavaScript звучит так: она уходит из продукта и остаётся в проверках, как второе мнение, а не как свидетель. Это не компромисс из осторожности — это единственный ход, который сохраняет свойство.
Три замены рассмотрены и отвергнуты, каждая с доводом:
| ход | что ловит | почему не годится |
|---|---|---|
| печатать компилятор в две разные цели и сверять их | ошибки генератора кода | исходник на flang у обеих целей один и тот же; устойчивая ошибка воспроизведётся в обеих |
| сверять текущий компилятор с предыдущим выпуском | откаты и случайные регрессии | устойчивая ошибка была и в предыдущем — она сойдётся |
| точка раскрутки в C как вторая реализация | зависимость от хозяина (Node) | порождена из тех же исходников на flang; независим сборщик, а не источник |
Общий довод у всех трёх один: независимость должна быть в источнике, а не в пути сборки. Две дороги из одной точки приводят в одну точку.
Чем подтверждено. Рассуждением, а не прогоном, — и это сказано прямо. Прогоном подтверждена только польза второй реализации, пока она есть: 15 828 сверок ядра доказательства, 4 480 ответов вычислителя, 243 программы обязательств, 2 318 примеров — все расхождения ловились именно сравнением двух порознь написанных реализаций.
Чем ограничено — и это важнее самого решения. Второе мнение перестаёт работать не тогда, когда его удалят, а тогда, когда его перестанут догонять. Отставший свидетель молчит так же, как отсутствующий. За одну сборку это случилось пять раз подряд с одним и тем же слоем. Значит отставание надо мерить и называть числом — как названы 12 программ зазора ядра, — а не оговаривать словами.
Отсюда практическое правило: побайтовая сверка живёт дольше того, кого она сверяет. Убирая реализацию из продукта, её сверку не убирают, а переворачивают: истина — ответ слоя на самом языке, вторая реализация — свидетель, и чинят того, кто разошёлся с языком.
Связано: byte-for-byte-comparison, twin-lags-behind-the-reference, four-pieces-of-javascript, byte-comparison-misses-object-identity, proven-is-not-correct