Язык, который
говорит прямо
Nova — язык системного уровня на основе алгебраических эффектов, статических контрактов и M:N рантайма. Каждый побочный эффект объявлен в сигнатуре. Каждый инвариант проверяется компилятором.
// Алгебраические эффекты в сигнатурах
fn fetch_user(id u64) 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 доказываются SMT-решателем на этапе компиляции, при необходимости проверяются в рантайме в режиме отладки и удаляются без накладных расходов в релизе.
M:N Рантайм
Файберы поверх системных потоков с планировщиком на основе похищения задач. Память управляется автоматически (Boehm GC сейчас, инкрементальный GC в планах). Для путей с жёсткими требованиями по задержке — realtime nogc.
Для эпохи ИИ
Код пишет ИИ. Проверяет человек.
Всё больше кода генерируется ИИ. Но проверяет его по-прежнему человек. Nova — первый язык, явно оптимизированный для этого: побочные эффекты объявлены в сигнатуре, поэтому ревью остаётся локальным — читаешь функцию, а не весь граф вызовов.
Побочные эффекты указаны в сигнатуре — между параметрами и стрелкой возврата. Ревью становится локальным: видно, что делает функция, без чтения её тела.
Любую зависимость можно подменить через блок with — та же бизнес-логика работает с реальной базой в продакшене и с in-memory обработчиком в тестах. Мокинг-библиотеки не нужны.
parallel for запускает итерации параллельно со структурным скоупингом. Функциям не нужно ключевое слово async — приостановка амбиентная. Нет «заражения» async.
Контракты опциональны — добавляй requires и ensures там, где нужно. Компилятор доказывает их статически когда может; то, что доказать не удалось, становится проверкой в рантайме.
Эффекты в деле
Все зависимости видны с первого взгляда
Сигнатура HTTP-сервера сообщает, что он работает с сетью (Net), говорит на HTTP (Http) и пишет логи (Log). Ничего неявного. Система эффектов и есть документация.
// HTTP-сервер — эффекты видны в сигнатуре
fn serve_api() Net Http Log -> ()
{
let router = Router.new()
.route(Get, "/users/:id", get_user)
.route(Post, "/users", create_user)
Http.serve("0.0.0.0:8080", router.dispatch())
}Попробовать Nova
Nova — pre-alpha, компилятор собирается из исходников. Подробные шаги на странице установки.
git clone https://github.com/nv-lang/nova && cd nova/nova-cli && cargo build --release
Собирает CLI nova · требования и первая программа
Присоединиться
Nova — открытый проект, разрабатываемый публично. Следите за дизайном языка, сообщайте об ошибках, вносите код или просто наблюдайте за ростом компилятора.