Система · проект, не входит ни в один выпуск
LSPE
Каждая сборка — это набор решений о вашей программе. LSPE заставляет компилятор отвечать за них: он ищет источник каждого решения, задаёт вам записываемый вопрос, когда источника нет, и вписывает этот обмен в бинарник. Он не обещает, что программа верна. Он обещает, что ни одно исключение не останется невысказанным.
Это проект, а не то, что можно скачать
На 2026-10-18 LSPE — это проект. Ни один выпуск его не содержит, устанавливать нечего, и на этой
странице нет даты, когда он появится. Сам проект записан в репозитории как docs/262
— по-китайски, как и остальные нумерованные проектные документы: этот проект держит планы
там, а не в публичном трекере задач.
Дальше — то, для чего этот проект, и то, от чего он отказывается. Это не объявление о функции, которую можно включить.
Проект — не обещание. Две вещи уже известны как невозможные, и проект записывает их, а не обходит: ни один компилятор не докажет, что программа свободна от дефектов, и ни один компилятор не ответит на все вопросы, на которые сам ответить не может. Всё ниже определено этими двумя фактами.
Чек на каждое решение
Сегодня компилятор даёт вам один бит: программа принята или отвергнута. Причины остаются внутри компилятора, а допущения, на которых он дошёл до «принята», не записаны нигде, где вы могли бы их проверить.
LSPE добавляет запись. Каждый раз, когда компилятор пропускает то, что доказать не смог, бинарник записывает, какое это было решение, на каких свидетельствах оно держалось и — если на вопрос отвечал человек — кто ответил. В бинарнике лежит хеш этой записи; дерево вывода остаётся рядом, вне бинарника, поэтому бинарник от него не растёт.
Это не «нет дефектов». Есть ли в программе дефекты, компилятор решить не может; записано ли каждое исключение — может. Первое неразрешимо. Второе — свойство процесса, и его можно проверить офлайн, задним числом, силами того, кто компилятору не доверяет.
Четыре части
LSPE — это четыре вещи, работающие в одном пространстве: точки в модуле, где было принято решение, обязательства этих точек, свидетельства в их пользу и запись о том, что с каждой точкой стало. Это не пятая проверка. Проверки остаются на своих местах.
Вопрошающий
Компилятор перестаёт быть только судьёй. Прежде чем принять решение, он ищет для него источник, пытается построить контрпример и сверяет его со второй реализацией. Если не выходит всё три, у него есть дыра — и он говорит об себе, а не о том, что ваш код плох.
Вопросы
Дыра становится вопросом с вариантами, значением по умолчанию и последствием каждого ответа. Ваш ответ записывается. Отсрочка без записи — сама по себе ошибка компиляции, так что «я знаю, что здесь подозрительно, но не могу объяснить» перестаёт быть знанием, живущим только в чьей-то голове.
Полиция LSPC
Перед сборкой она подаёт счёт: какие остаточные риски вы собираетесь принять, по строке на семейство, с тем, что случится, если семейство не выполнится. По умолчанию она не блокирует. Что хотите — чините, остальное оставляете, и оставленное записывается.
Журнал
Всё, что решают другие компоненты безопасности — лестница возврата памяти, уровни безопасности памяти, домены возможностей, владение — приходит в один журнал. Ни один из этих компонентов не заменяется и не переименовывается; журнал — место, где их решения можно прочитать вместе и сверить.
Бремя доказывания меняет направление
Обычный компилятор стоит вне программы и объявляет результат. LSPE сидит внутри сделки: называет свой источник, назначает цену своим допущениям и выдаёт вам чек. Когда доказать не может, он не вправе сказать «ваш код неверен»; он должен сказать «в моём доказательстве здесь дыра». Первое — утверждение о вас, второе — о компиляторе, и эти два намеренно разделены.
У этого разделения есть цена, и проект её платит: вопрошающий ведёт журнал каждой подстановки типов и заново доказывает обязательства после каждой. В собственной истории Rust есть дефект целостности ровно такой формы — проверка, которая выполнялась до подстановки, не была запущена после неё. Компилятор, который спрашивает только «есть ли источник?», этого не поймает: источник был, но истёк.
Продавец — не власть. Семантика принадлежит стандарту и каждому компоненту. LSPE записывает решения и назначает им цену; он не решает, что истинно.
Чего он не делает
Он не находит больше ошибок памяти
Он находит исключения без источника и свидетельства с истёкшим сроком. Программа без таких исключений всё равно может быть неверной.
Он не делает программу безопаснее
Он делает невозможным принять остаточный риск молча. Это два разных числа, и проект держит их раздельно, а не обменивает одно на другое.
Он не заменяет проверки
Лестница возврата памяти, уровни безопасности памяти, домены возможностей и владение сохраняют свои имена, своих владельцев и свои критерии. LSPE читает их решения.
Это не способ проверять меньше
Закрыть аудит — это записанный выбор, под которым вы подписываетесь, а не переключатель, убирающий проверки. Проверки идут в любом случае; меняется только то, записан ли результат.
Лестница возврата памяти описана на своей странице, а власть для каждого
обязательства — это стандарт. Проектный документ —
docs/262 в репозитории.