Topazdocs
Обзор

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

Одна спецификация. Два движка. Ноль расхождений. Topaz — исполняемый язык спецификаций для детерминированного программного обеспечения.

Topaz — это исполняемый язык спецификаций для детерминированного программного обеспечения: читаемый как спецификация, запускаемый как оракул и дифференциально протестированный против продакшн-реализаций.

Topaz не пытается обогнать Rust. Это неверная постановка вопроса. Topaz существует, чтобы сделать намерение достаточно точным, чтобы люди могли его читать, агенты — писать, а тулчейн — проверять то, что продакшн-код заявляет как свою реализацию.

Эта архитектура движется в три такта: спецификация, ориентированная на человека, исполняемый оракул и дифференциальная верификация.

1. 正 Спецификация, ориентированная на человека

Большинство языков пишутся машинно-ориентированно. Вы описываете, что должно делать железо, а само намерение — правило, политика, домен — остаётся неявным, спрятанным внутри потока управления.

Topaz переворачивает порядок. Намерение приходит первым, и оно записывается на языке задачи, а не на языке железа.

Доменные слова — это код. 한글, Кириллица и эмодзи являются идентификаторами первого класса, а не лазейками. Unicode-first — это не украшение. Это способ сохранить правила без потерь при переводе.

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

В результате сложная логика — корейская типографика, правила, привязанные к локали, и трудные бизнес-случаи — читается как само правило. Спецификация должна быть читаемой, прежде чем ей можно будет доверять.

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

Спецификация, которая живёт только в документе, — это мёртвая спецификация. Она отдаляется от кода. В конце концов она начинает лгать.

Topaz отказывается быть мёртвой спецификацией. Каждое написанное вами правило выполняется.

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

Topaz — это документ, который вычисляет ответ.

Эта инверсия важна. Спецификация — это не документация, которая плетётся за реализацией. Спецификация — это эталон, которому должна соответствовать реализация. Когда вы хотите узнать, что значит «правильно», вы не начинаете с чтения Rust. Вы спрашиваете Topaz.

3. 合 Дифференциальная верификация (run ≡ build)

Продакшн по-прежнему требует быстрого пути. Поэтому Topaz эмитит продакшн-путь на Rust, сохраняя интерпретатор как эталонный путь выполнения.

Но доверенный перевод — это не верификация. topaz run и topaz build должны проверяться друг против друга.

В CI корпус и golden-фикстуры подают на оба пути одни и те же входные данные. Дифференциальный харнесс сравнивает значение, stdout, файлы, сбои и span байт за байтом. Один и тот же ввод должен давать один и тот же наблюдаемый результат, иначе сборка не проходит.

Это и есть run ≡ build.

Это не лозунг. Это обязательство верификации, которое тулчейн обязан выполнить. Интерпретатор говорит, что истинно. Путь на Rust говорит это быстро. Харнесс проверяет, что это одно и то же предложение.

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

Вы пишете намерение. Компилятор пишет Rust. Тулчейн доказывает, что они согласуются.

4. Почему маленький язык

Малость — это не эстетическое предпочтение. В Topaz малость — это граница верификации.

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

Это существующая идентичность Topaz, поднятая до уровня исполняемой архитектуры.

Один канонический способ сказать каждую вещь. Доменные слова сохраняются на языке домена. Unicode-first начиная с лексера. Люди и агенты пишут одну и ту же поверхность, а тулчейн её проверяет.

Topaz намеренно мал, потому что цель не в том, чтобы выразить любой возможный стиль программирования. Цель в том, чтобы сделать намерение достаточно стабильным, чтобы его можно было выполнить и проверить.

5. ATLAS как продакшн-пример доказательства

ATLAS — это первый продакшн-пример доказательства этой архитектуры.

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

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

ATLAS — это первый продакшн-пример доказательства. Он не должен стать последним.

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

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

Вы пишете правило один раз, на маленьком Unicode-first языке. Интерпретатор делает его запускаемым. Компилятор пишет Rust. CI сравнивает эталонный путь и продакшн-путь байт за байтом.

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