Дорога до 1.0

Сейчас вышла версия 0.7.29. Ниже — что войдёт в 0.8, 0.9 и 1.0, в каком порядке и к какому сроку. Сроки — ориентир ведущего, а не обещание: каждая полоса закрывается прогоном, который можно повторить, и пока прогон не зелёный, полоса не считается закрытой. Что язык уже умеет, читают не здесь: Справочник конструкций, Установка, Выпуски.

Что значит 1.0

Семь условий, и каждое проверяется командой, а не словом:

1. Компилятор собирает сам себя воспроизводимо. Две печати из одного дерева дают один и тот же C, и CI это сравнивает на каждом выпуске.
2. Перепечатка дешёвая. Полная печать компилятора занимает меньше часа на обычной машине (сегодня — около 80 минут на сервере сборки).
3. Ядро доказательств доказано. У каждого правила, которым ядро закрывает утверждение, есть теорема в Lean, проверяемая чужим ядром; и есть вторая, независимая проверка записи.
4. Известных дыр типизации нет. Каждая найденная дыра либо закрыта, либо названа в справочнике отказов с номером.
5. Форматы устойчивы. Коды отказов, запись доказательства и промежуточный вид не меняются без новой старшей версии.
6. Пакеты полноценны. Поиск по имени, установка, разрешение версий, замок зависимостей.
7. Язык в работе. Несколько настоящих служб, которые живут месяцами и которые чинят, когда они падают.

0.7.25 — точные числа (октябрь 2026, выходит)

• точное целое и точное дробное: сложение, вычитание, умножение, деление дроби и порядок без потолка 2^53; (1/10 + 1/5) + 3/10 и 1/10 + (1/5 + 3/10) дают одну и ту же дробь — то, чего над число (double) не бывает.
• Предел памяти и времени дочернему процессу называет сама программа, а не оболочка.
• Страница реестра пакетов печатается из списка имён и выкладывается на сайт.

0.8 — прибор (ноябрь 2026)

Что получит программист:

• Установка без компилятора C. В выпуске лежат готовые двоичные для Linux (x86_64, aarch64) и macOS (arm64, x86_64) с контрольными суммами; brew, asdf и прямая загрузка ставят один и тот же файл.
• Оснастка на самом языке. Проверки репозитория, стенды и сборка сайта исполняются планами на flang, а не sh и JavaScript; оболочка остаётся там, где она судит сам компилятор, и это названо поимённо.
• Чистые имена. Ключи команд, коды отказов и имена в скриптах — английские слова.
• Ядро умеет больше. Законы поля над точным дробным; перебор конечного типа; линейная арифметика от допущений; переписывание цели по доказанным равенствам.
• Проверка записи доказана целиком. Для каждого приёма независимой проверки есть лемма в Lean, и отдельная проверка краснеет, если приём появился без леммы.

0.9 — доказательства (февраль 2027)

• Индукция по натуральным и по своим типам внутри доказательства; доказанное завершение по объявленной мере — как теорема, а не как объявление.
• Кванторы внутри формул и существование без названного свидетеля.
• Вторая реализация проверки записи доказательства, написанная не на C: расхождение двух проверок видно на каждом выпуске.
• Пакеты: flang package ставит, разрешает версии и пишет замок.
• Законы моноида и монады судит ядро, а не пример.

1.0 (весна 2027)

• Воспроизводимая самосборка в CI, печать меньше часа.
• Замороженные форматы отказов и записи доказательства.
• Три службы в работе месяцами — это условие закрывают пользователи, а не ведущий, поэтому оно единственное, у которого нет точной даты.

Что решено не делать

• Замыканий не будет. Захват окружения ломает доказательство завершения и прямую печать в C, Go и Rust; функции-значения есть, замыканий нет.
• Двух версий одной библиотеки в одной программе не будет — поднимается версия.
• Хранить код в базе вместо файлов (как Unison) не будем — берём только адресацию по содержимому.

Как проверить любую строку выше: у каждой полосы есть задача в docs/tasks/ и решение в docs/adr/; закрытие — зелёный прогон, который называет страница Выпуски.