Nova — язык системного уровня на основе алгебраических эффектов, статических контрактов и M:N рантайма. Каждый побочный эффект объявлен в сигнатуре. Каждый инвариант проверяется компилятором.
// Алгебраические эффекты в сигнатурах
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)
}
}Зачем Nova
Три примитива на уровне языка, меняющих способ рассуждений о программах.
Сеть, ввод-вывод, случайность, время и мутация появляются прямо в типе функции — между параметрами и стрелкой возврата. Никакого скрытого control flow. Никаких неожиданных await. Вызывающий всегда знает, что делает функция.
Клаузы requires, ensures и invariant проверяются SMT-решателем на этапе компиляции, при необходимости верифицируются в runtime в debug-режиме и стираются с нулевой стоимостью в release.
Go-style файберы поверх OS-потоков с work-stealing планировщиком. Managed-память по умолчанию (Boehm GC сейчас, concurrent GC в планах). Для latency-sensitive путей — realtime nogc.
Эффекты в деле
Сигнатура 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)
serve("0.0.0.0:8080", router.dispatch())
}Установить компилятор одной командой. Работает на Linux и macOS.
curl -sSf https://nv-lang.org/install.sh | sh
Nova — открытый проект, разрабатываемый публично. Следите за дизайном языка, сообщайте об ошибках, вносите код или просто наблюдайте за ростом компилятора.