Язык, который
говорит прямо
Nova — язык системного уровня на основе алгебраических эффектов, статических контрактов и M:N рантайма. Эффекты видны в типах; опциональные контракты проверяются там, где компилятор может их доказать.
// Алгебраические эффекты в сигнатурах
fn fetch_user(id int) Db Log -> Result[User, NotFound]
requires id > 0
{
Log.info("fetching ${id}")
match Db.find_user(id) {
Some(u) => Ok(u)
None => Err(NotFound)
}
}Зачем Nova
Простые правила, сильные гарантии
Три примитива на уровне языка, меняющих способ рассуждений о программах.
Алгебраические эффекты
Сеть, ввод-вывод, случайность, время и мутация появляются прямо в типе функции — между параметрами и стрелкой возврата. Никакого скрытого control flow. Никаких неожиданных await. Вызывающий всегда знает, что делает функция.
Статические контракты
requires, ensures и invariant задают опциональные контракты. Проверка Oracle по умолчанию покрывает тривиальные случаи; для более сложных доказательств нужен опциональный Z3. Недоказанные условия проверяются в рантайме в предусмотренных режимах; эти проверки снимаются в release-сборках.
M:N Рантайм
Файберы поверх системных потоков с планировщиком на основе похищения задач. Память управляется автоматически (Boehm GC сейчас, инкрементальный GC в планах). Для путей с жёсткими требованиями по задержке — функции #realtime; режим без GC-аллокаций (nogc) — в планах.
Для эпохи ИИ
Код пишет ИИ. Проверяет человек.
Всё больше кода генерируется ИИ. Но проверяет его по-прежнему человек. Nova — первый язык, явно оптимизированный для этого: побочные эффекты объявлены в сигнатуре, поэтому ревью остаётся локальным — читаешь функцию, а не весь граф вызовов.
Побочные эффекты указаны в сигнатуре — между параметрами и стрелкой возврата. Ревью становится локальным: видно, что делает функция, без чтения её тела.
Любую зависимость можно подменить через блок with — та же бизнес-логика работает с реальной базой в продакшене и с in-memory обработчиком в тестах. Мокинг-библиотеки не нужны.
parallel for запускает итерации параллельно со структурным скоупингом. Функциям не нужно ключевое слово async — приостановка амбиентная. Нет «заражения» async.
Контракты опциональны — добавляй requires и ensures там, где нужно. Oracle доказывает то, что умеет выбранный backend; резервные проверки рантайма снимаются в release-сборках.
Эффекты в деле
Все зависимости видны с первого взгляда
Первая строка — fn main() Net Time Detach — объявляет всё, что эта программа делает с внешним миром: сеть (Net), время (Time), откреплённые файберы соединений (Detach). Ничего неявного. Система эффектов и есть документация.
// HTTP-сервер — все зависимости в сигнатуре
fn main() Net Time Detach -> () {
ro app = Router.new()
.get("/users/{id}", get_user)!!
.post("/users", create_user)!!
consume listener = TcpListener.bind("0.0.0.0:8080")!!
serve_router(listener, app, ServerPolicy.new())
}Попробовать Nova
Начните с бинарного альфа-архива Oracle 0.1.0 для Windows или Linux x86_64. Нужен системный C-компилятор; предварительно собирать компилятор на Rust не требуется.
Скачать Oracle и посмотреть Carina
Настройка и первая программа · Сверяйте архив с SHA256SUMS его выпуска
Присоединиться
Nova — открытый проект, разрабатываемый публично. Следите за дизайном языка, сообщайте об ошибках, вносите код или просто наблюдайте за ростом компилятора.