Ник Матсакис предлагает для Rust северную звезду эпохи ИИ-агентов: ноль unsafe-кода

Один из ключевых людей в дизайне Rust опубликовал текст о том, что кодинг-агенты значат для языка. Это письменная версия доклада на REBASE в рамках SPLASH. Сам автор называет содержимое «недопечёнными идеями», так что это видение, а не предложение новых фич.

Выводы такие: люди в программировании всё ещё нужны, дизайн языков по-прежнему важен, а Rust хорошо подходит для агентной разработки и может подойти ещё лучше.

По производительности аргумент простой. Хорошие значения по умолчанию плюс явные ручки для тонкой настройки. По словам автора, люди, которые раньше вручную оптимизировали криптографический код, теперь обращаются к агентам. Вместе с профайлером вроде dial9 получается цикл: бенчмарк, профиль, агент предлагает правку, PR в репозитории.

С надёжностью сложнее. Типы удерживают агента в рамках, но тесты показывают наличие багов, а не их отсутствие, и типы гарантируют лишь отсутствие определённых классов ошибок, а не корректность результата. Тут нужны доказательства. Для Rust уже есть Verus, Creusot, Aeneas и Kani. При этом типы продолжают играть роль, потому что делают доказательства дешевле. &mut даёт гарантию уникальности, и Verus опирается на borrow checker именно ради этого, чтобы солверу было проще.

Куда, по мнению Матсакиса, стоит двигаться: более выразительная система типов (view types, внутренние ссылки, даже проверка вроде «в лог не попадают персональные данные»), расширяемый компилятор, чтобы инструменты доказательств не жили на костылях из макросов и привязке к конкретным версиям компилятора, и поддержка доказательства корректности unsafe-кода.

Северная звезда: больше никакого unsafe. Это не значит убрать ключевое слово. Это значит уметь доказать, что весь unsafe-код корректен и не приводит к неопределённому поведению.

Главной открытой проблемой автор называет дизайн, то есть решение о том, что вообще строить. Ставка на специализированные языки дизайна, которые превращают высокоуровневое намерение в проверки типов, линты или теоремы.

Для контекста Матсакис цитирует Дэвида Толная: инженеры Meta в этом году написали первосторонний Rust-кода вдвое больше, чем за предыдущие девять лет вместе взятые.

Блог: https://smallcultfollowing.com/babysteps/blog

Источник: https://smallcultfollowing.com/babysteps/blog