Topazdocs
Обзор

Исполняемая спецификация

Один исходник. Один эталон. Проверяемые backend'ы. Топаз — исполняемый язык спецификаций для детерминированного программного обеспечения.

Топаз рассматривает исходный код как исполняемую спецификацию. Исходник должен быть достаточно читаемым, чтобы объяснить правило, достаточно точным, чтобы вычислить эталонный ответ, и достаточно стабильным, чтобы другая реализация могла доказать согласие с ним.

Эта страница не повторяет введение в язык. Она объясняет архитектуру.

1. Спецификация для человека

Полезной спецификации сначала нужно быть читаемой. Если важное правило похоронено под машинной церемонией, документ может исполняться, но он плохо работает как эталон для людей и агентов.

Топаз ставит доменное правило на первое место. Имена могут оставаться на языке предметной области. Грамматика остаётся достаточно малой, чтобы читателю не приходилось изучать новый диалект в каждом файле. Цель не в том, чтобы разрешить любой стиль программирования. Цель в том, чтобы правило было трудно понять неправильно.

2. Исполняемый оракул

Спецификация, которая живёт только в прозе, дрейфует. Сначала она говорит правду, затем постепенно превращается в рассказ о старой правде.

Топаз избегает этого, делая спецификацию запускаемой. Интерпретатор — эталонный путь: для заданного ввода он вычисляет наблюдаемый результат. Этот результат можно закрепить как фикстуру и сравнивать с любым более быстрым или низкоуровневым путём.

Когда вопрос звучит как «что это должно делать?», первый ответ должен приходить из исходника Топаза, а не из сгенерированного артефакта или ручного переноса.

3. Дифференциальная верификация

Продакшн всё равно требует скомпилированный путь. Поэтому Топаз разделяет роли:

  • topaz run выполняет эталонный путь через интерпретатор.
  • topaz build создаёт скомпилированный путь: нативный бинарник Rust или сгенерированный Python с --target python.

Эти пути не получают доверия по намерению. Их сравнивают. Дифференциальный харнесс подаёт интерпретатору и каждому backend одинаковые входные данные и проверяет наблюдаемые результаты байт в байт: значения, stdout, файлы, фолты и позиции в исходнике. Если backend расходится, эта сборка не доказала себя на измеренной поверхности.

Это смысл run ≡ build: не лозунг, а обязанность верификации, которую харнесс обеспечивает для каждой backend-цели.

4. Почему малость важна

Малость здесь не вопрос вкуса. Это граница, которая делает оракул пригодным.

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

Топаз остаётся малым, чтобы тулчейн мог давать более сильные обещания о коде, который остаётся.

5. ATLAS как доказательный случай

ATLAS — первый продакшн-пример этой модели. Он использует Топаз для сложных правил корейской типографики, держит интерпретатор как эталонный путь и сравнивает производительные пути на Rust с результатом Топаза через корпусные тесты, golden-фикстуры и дифференциальные проверки.

Утверждение намеренно узкое. ATLAS не доказывает, что любой дефект невозможен, и не валидирует Rust целиком. Он показывает, что реальный продукт может поставить Топаз в эталонное место, Rust — в продакшн-место, и требовать согласия до того, как продакшн-путь считается корректным.

6. Проверяемые backend'ы

Backend'ы Rust и Python расширяют эту модель на разные экосистемы. Эталоном остаются исходник Топаза и интерпретатор; Rust и Python — эмитируемые проверяемые артефакты, а не самостоятельные авторитеты. Backend Rust понижает до самостоятельного нативного бинарника, а backend Python нацелен на серверную, data и operations-работу.

Согласие — это то, что проверяет тулчейн, а не строка на сайте. Публичное свидетельство — receipt измеренной поверхности: на прогнанном наборе один и тот же исходник Топаза показывает одно наблюдаемое поведение и одно поведение runtime guards на путях интерпретатора, Rust и Python, при нуле тихих расхождений. Утверждение о полноте по всему, что принимает чекер, вне области; точную поверхность указывает страница состояния.

Это важно в проекте, где много работы делают агенты. Агенты быстро создают код, но скорость не доказательство. Второй проверяемый backend даёт ещё один исполняемый путь для ревью, отладки и несогласия. Если интерпретатор, путь Rust и путь Python расходятся, расхождение становится видимым.

7. Заключение

Топаз — место, где намерение становится исполняемым.

Вы пишете правило один раз. Интерпретатор вычисляет эталонный ответ. Эмиссия Rust проверяет нативный и системный путь дизайна. Эмиссия Python проверяет серверный и data-путь дизайна. Харнесс проверяет, что пути говорят одно и то же.

Одна спецификация. Несколько проверок эмиссией. Ноль расхождений.