Hello, Nova

Evgeniy Golovin 18 мая 2026 Объявление Язык

Сегодня мы открываем двери Nova — языку программирования общего назначения системного уровня, который мы публично разрабатываем уже год. В этом посте объясняется, что такое Nova, зачем он нужен и что уже работает прямо сейчас.

Nova — это не очередная «безопасная замена C» и не убийца JavaScript. Это язык, центральная ставка которого такова: если сделать побочные эффекты и инварианты первоклассными гражданами системы типов, можно устранить целые категории ошибок до того, как программа когда-либо запустится.

Проблема невидимого поведения

Большинство языков позволяют функциям лгать. Функция с именем get_user может обращаться к базе данных, делать HTTP-вызов, писать строку лога и кэшировать результат в глобальной карте — и ничего из этого не видно в её сигнатуре. Вызывающий не имеет возможности это узнать, не читая тело функции. Тесты вынуждены мокировать весь мир. Ревьюеры вынуждены держать в голове всё это.

Именно эту проблему призван решить Nova. В Nova каждый побочный эффект должен фигурировать в типе функции — между списком параметров и стрелкой возврата. Если функция обращается к базе данных, в её типе фигурирует Db. Если она пишет логи — так же и Log. Если не делает ни того ни другого, проверщик типов это доказывает.

Сигнатура — это не документация, которая может быть неверной, а ограничение, которое компилятор принудительно выполняет.

Три идеи, один язык

1. Алгебраические эффекты

Эффекты в Nova — это первоклассные интерфейсы. Вы объявляете эффект, предоставляете обработчик и внедряете его на границе вызова. Это даёт вам всю мощь внедрения зависимостей без бюрократии — и система типов отслеживает это автоматически.

fetch_user.nv

// Сигнатура — это контракт с вызывающим:
// дай мне положительный id, я верну тебе User или NotFound,
// и я затрону только Db и Log — и ничего больше.
fn fetch_user(id u64) Db Log -> Result[User, NotFound]
    requires id > 0
{
    log("fetching", {id: id.to_str()})
    match db.find_user(id) {
        Some(u) => Ok(u)
        None    => Err(NotFound)
    }
}

Пользовательские эффекты позволяют моделировать любую возможность как абстрактный интерфейс. Тестирование становится тривиальным: замените продакшн-обработчик Db на in-memory вариант на сайте вызова, и вы получите полную изоляцию без фреймворка для моков.

2. Статические контракты

Контракты Nova — это клаузы requires, ensures и invariant, прикреплённые к функциям и типам. Компилятор передаёт их SMT-решателю (сейчас Z3) и пытается проверить их на этапе компиляции. Когда статическая проверка невозможна — как правило, потому что ограничения зависят от данных рантайма — они переходят к проверочным утверждениям рантайма в debug-сборках и стираются в release-сборках.

Ключевое понимание: контракты — это не утверждения. Утверждение — это проверка в рантайме, которую вы добавляете постфактум. Контракт — это спецификация, которую вы пишете рядом с кодом, и компилятор использует её для рассуждений через границы вызовов. Функция, вызывающая fetch_user с литеральным 0, получает ошибку компиляции, а не панику в рантайме.

3. M:N Рантайм

Рантайм Nova мультиплексирует лёгкие файберы поверх OS-потоков с помощью work-stealing планировщика — та же модель, что освоил Go, применённая к статически типизированному языку с эффектами. Порождение файбера дёшево (несколько сотен наносекунд). Блокировка на I/O уступает файбер, и планировщик запускает другую работу на том же потоке. Никаких ключевых слов async. Никаких раскрашенных функций. Блокирующий код и конкурентный код выглядят одинаково.

server.nv

// Полный набор возможностей — в сигнатуре.
// Никаких скрытых глобальных переменных. Никакого неявного async рантайма.
fn serve_api() Net Http Log -> ()
{
    let router = Router.new()
        .route(Get,  "/users/:id", get_user)
        .route(Post, "/users",    create_user)

    serve("0.0.0.0:8080", router.dispatch())
}

Для чувствительной к задержкам работы можно аннотировать функцию realtime nogc, чтобы сообщить компилятору и рантайму, что никаких GC-управляемых аллокаций в этой области не допускается. Компилятор проверяет это статически. Конкурентный игровой цикл, DSP-коллбэк, lock-free очередь — всё это первоклассные варианты использования, а не запоздалая мысль.

Что работает сегодня

Nova находится на стадии bootstrap. Это означает, что компилятор существует и компилирует реальные программы, но стандартная библиотека неполна, а поверхность языка ещё стабилизируется. Вот честный отчёт о том, что работает:

Основная система типов — структуры, перечисления, дженерики, трейты, Option[T], Result[T, E], вывод типов и сопоставление с образцом — всё работает.
Эффекты — типы эффектов в сигнатурах функций принудительно проверяются проверщиком типов. Встроенные эффекты (Io, Net, Db, Log, Rand, Time, Fs) распознаются. Пользовательские эффекты с кастомными обработчиками работают в текущем компиляторе.
Контракты — клаузы requires и ensures парсятся и проверяются. Интеграция SMT (Z3) функциональна для линейной арифметики. Откат к рантайму для недоказуемых ограничений работает. Структурный invariant реализован и принудительно выполняется (включая правило, что избыточные спецификации полей отклоняются).
M:N рантайм — файберный планировщик работает, spawn функционирует, каналы можно использовать. Work-stealing по потокам реализован. I/O является файбер-совместимым на Linux (io_uring) и macOS (kqueue).
Инструменты документирования — nv doc генерирует HTML-документацию из doc-комментариев. Формат задан в D45.
Стандартная библиотека — core (типы, трейты), io (базовый файловый и консольный I/O), net (TCP-сокеты) и collections (Vec, Map, Set) готовы к использованию. HTTP, крипто и драйверы баз данных в разработке.

Что ещё не готово: стабильный пакетный менеджер, языковой сервер, поддержка Windows и конкурентный GC (текущий GC — Boehm, который stop-the-world). Всё это в ближайшем roadmap.

Эффекты и контракты вместе

Настоящая мощь Nova проявляется, когда эффекты и контракты работают вместе. Рассмотрим функцию, которую можно вызывать только внутри аутентифицированного контекста запроса и которая должна обращаться только к базе данных:

billing.nv

fn charge_card(
    ctx    AuthCtx,
    amount Money,
    card   CardToken,
) Db Net Log -> Result[ChargeId, PaymentError]
    requires ctx.is_authenticated()
    requires amount > Money.ZERO
    requires amount <= Money.MAX_SINGLE_CHARGE
{
    log("charging", {user: ctx.user_id.to_str(), amount: amount.to_str()})
    let result = payment_gateway.charge(card, amount)?
    db.record_charge(ctx.user_id, result.id, amount)?
    Ok(result.id)
}

Предусловия (requires) точно сообщают вызывающим, что должно быть истинным перед вызовом. Эффекты в типе перечисляют каждую внешнюю систему, к которой обращается функция. Ревьюер кода — или LLM, генерирующий вызывающий код — может понять полный контракт только из сигнатуры, не читая тело.

Почему именно сейчас?

Два тренда сходятся, делая это правильным временем для Nova.

Во-первых, инструменты для принудительного выполнения этих ограничений созрели. SMT-решатели, такие как Z3 и CVC5, достаточно быстры для работы в цикле обратной связи компилятора. Системы алгебраических эффектов переместились из академических статей в продакшн-компиляторы (Koka, Effekt, OCaml 5). Кусочки существуют; Nova собирает их в практический язык.

Во-вторых, LLM теперь пишут значительную долю продакшн-кода. Код, генерируемый LLM, как правило, синтаксически правильный, но семантически недоспецифицированный — эффекты и инварианты находятся в голове программиста, а не в коде. Язык, где эффекты и контракты обязательны, а не опциональны, превращает ошибки компилятора в обучающий сигнал как для людей, так и для моделей. Nova создан для эпохи, когда компилятор является основным ревьюером.

Что дальше

Ближайший roadmap (Планы 60—64 в репозитории) включает:

Пакетный менеджер nv: формат манифеста, разрешение зависимостей и публичный реестр
Языковой сервер (nova-lsp): дополнения кода, переход к определению, встроенная диагностика контрактов
Конкурентный GC на замену Boehm
Поддержка тулчейна Windows
Завершение стандартной библиотеки: HTTP сервер/клиент, TLS, SQL и сериализация

Спецификация открыта, компилятор с открытым исходным кодом, и процесс проектирования происходит на GitHub. Если всё это резонирует с вами, лучший способ следить за развитием — поставить звезду репозиторию и читать D-блоки.

Мы также принимаем контрибуции. В руководстве для контрибьюторов объясняется, где сейчас нужна помощь больше всего.

Язык молод. Идеи — нет. Мы с нетерпением ждём возможности строить его вместе с вами.

— Evgeniy Golovin, 18 мая 2026

Смотреть на GitHub Читать документацию Спецификация языка