Язык, который
говорит прямо
Nova — язык системного уровня на основе алгебраических эффектов, статических контрактов и M:N рантайма. Каждый побочный эффект объявлен в сигнатуре. Каждый инвариант проверяется компилятором.
// Алгебраические эффекты в сигнатурах
fn fetch_user(id u64) Db Log -> Result[User, NotFound]
requires id != 0
{
Log.info("fetching ${id}")
match find_user(id) {
Some(u) => Ok(u)
None => Err(NotFound)
}
}Зачем Nova
Простые правила, сильные гарантии
Три примитива на уровне языка, меняющих способ рассуждений о программах.
Алгебраические эффекты
Сеть, ввод-вывод, случайность, время и мутация появляются прямо в типе функции — между параметрами и стрелкой возврата. Никакого скрытого control flow. Никаких неожиданных await. Вызывающий всегда знает, что делает функция.
Статические контракты
Аннотации requires, ensures и invariant доказываются SMT-решателем на этапе компиляции. Доказанные контракты удаляются без накладных расходов; недоказанные остаются fail-fast-проверками в рантайме — в том числе в релизной сборке.
M:N Рантайм
Файберы поверх системных потоков с планировщиком на основе похищения задач. Память управляется автоматически (Boehm GC сейчас, инкрементальный GC в планах). Для путей с жёсткими требованиями по задержке — функции #realtime; режим без GC-аллокаций (nogc) — в планах.
Для эпохи ИИ
Код пишет ИИ. Проверяет человек.
Всё больше кода генерируется ИИ. Но проверяет его по-прежнему человек. Nova — первый язык, явно оптимизированный для этого: побочные эффекты объявлены в сигнатуре, поэтому ревью остаётся локальным — читаешь функцию, а не весь граф вызовов.
Побочные эффекты указаны в сигнатуре — между параметрами и стрелкой возврата. Ревью становится локальным: видно, что делает функция, без чтения её тела.
Любую зависимость можно подменить через блок with — та же бизнес-логика работает с реальной базой в продакшене и с in-memory обработчиком в тестах. Мокинг-библиотеки не нужны.
parallel for запускает итерации параллельно со структурным скоупингом. Функциям не нужно ключевое слово async — приостановка амбиентная. Нет «заражения» async.
Контракты опциональны — добавляй requires и ensures там, где нужно. Компилятор доказывает их статически когда может; то, что доказать не удалось, становится проверкой в рантайме.
Эффекты в деле
Все зависимости видны с первого взгляда
Первая строка — 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
Nova — pre-alpha, компилятор собирается из исходников. Подробные шаги на странице установки.
git clone https://github.com/nv-lang/nova && cd nova/nova-cli && cargo build --release
Собирает CLI nova · требования и первая программа
Присоединиться
Nova — открытый проект, разрабатываемый публично. Следите за дизайном языка, сообщайте об ошибках, вносите код или просто наблюдайте за ростом компилятора.