Введение

Nova — язык программирования общего назначения системного уровня, построенный вокруг трёх ключевых идей: алгебраические эффекты, статические контракты и лёгкий M:N рантайм. Эти три примитива устраняют наиболее распространённые источники ошибок в программном обеспечении — скрытое поведение, нарушенные инварианты и непреднамеренную блокировку — на уровне языка, а не как библиотечные соглашения.

Nova нацелена на область, где нужен контроль системного уровня (предсказуемая производительность, явное управление ресурсами), но также желательны гарантии безопасности, которые обеспечивает современная теория типов. Это не исследовательский язык — он компилируется в нативный код и предназначен для создания реального программного обеспечения.

Установка

Nova — pre-alpha, CLI nova собирается из исходников (стабильный Rust 1.85+; для компиляции программ нужен C-тулчейн — Clang, MSVC или GCC):

git clone https://github.com/nv-lang/nova
cd nova/nova-cli
cargo build --release

CLI nova будет в nova-cli/target/release/nova; добавьте его в PATH. Подробные шаги — на странице установки.

Hello, World

Создайте файл hello.nv:

fn main() {
    println("Hello, World!")
}

Скомпилируйте и запустите:

nova build hello.nv
./hello

Точка входа программы — fn main(); println выводит строку в стандартный вывод.

Следующие шаги

Разделы руководства по языку ниже подробно объясняют эффекты, контракты, систему типов и модель конкурентности. Для формального описания каждой конструкции языка смотрите Спецификацию языка.

Если вы предпочитаете учиться на коде, в директории examples на GitHub есть аннотированные программы, охватывающие основные возможности языка.

Эффекты

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

Io — стандартный ввод/вывод (консоль, файлы)
Net — доступ к сети (сокеты, DNS)
Http — HTTP-клиент и серверные примитивы
Db — подключения к базам данных
Fs — доступ к файловой системе
Log — структурированное логирование
Rand — генерация случайных чисел
Time — системное и монотонное время
Mut — мутация разделяемого состояния (неявно в локальной области)

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

type Cache effect {
    get(key str) -> Option[[]u8]
    set(key str, val []u8) -> ()
}

// Эффекты Cache и Db берутся из активной with-области.
fn get_profile(user_id u64) Cache Db -> Profile
{
    let key = "profile:${user_id}"
    if let Some(raw) = Cache.get(key) {
        return Profile.decode(raw)
    }
    let rows = Db.query(sql`SELECT * FROM profiles WHERE id = ${user_id}`)
    let p = Profile.from_row(rows[0])
    Cache.set(key, p.encode())
    p
}

Контракты

Контракты Nova выражают машинно-проверяемые намерения прямо на границах функций. Три вида:

requires <expr> — предусловие; должно выполняться при вызове функции
ensures <expr> — постусловие; должно выполняться при нормальном возврате функции
invariant <expr> — инвариант типа; должен выполняться для каждого значения типа

Компилятор проверяет контракты через SMT-решатель на этапе компиляции — доказанные стираются в релизной сборке без затрат во время выполнения. Если решатель не может принять решение, контракт автоматически откатывается до проверки во время выполнения в отладочных сборках. Атрибут #must_verify на функции требует статического доказательства — компиляция прерывается, если решатель не справился.

fn sqrt(x f64) -> f64
    requires x >= 0.0
    ensures  result >= 0.0
{
    // компилятор знает, что x неотрицательно
    x.sqrt()
}

Типы

Nova имеет статическую систему типов с выводом типов, алгебраическими типами данных, дженериками и протоколами.

Примитивы: int, i8 i16 i32 i64, u8 u16 u32 u64, f32 f64, bool, char, str
Алгебраические типы: единый keyword type — type X { ... } для записей (произведений), type X | A | B для sum-типов (помеченных объединений); без struct/enum
Option и Result: Option[T] и Result[T, E] — встроенные sum-типы, никакого null
Дженерики: параметрический полиморфизм с ограничениями протоколов
Протоколы: структурные интерфейсы — любой тип с подходящими методами соответствует автоматически

Конкурентность

Рантайм Nova распределяет файберы — лёгкие потоки, которыми управляет сам рантайм — поверх потоков ОС с помощью планировщика с перехватом задач. Файбер порождается командой spawn, общается через каналы:

// parallel for запускает каждую итерацию как файбер и собирает результаты
let squares = parallel for i in 0..8 { i * i }
// squares == [0, 1, 4, 9, 16, 25, 36, 49]

// spawn — запустить и не ждать; supervised дождётся всех файберов
let mut count = 0
supervised {
    spawn { count = count + 1 }
    spawn { count = count + 1 }
}
// count == 2

Память

Nova использует управляемую память по умолчанию. Текущий рантайм интегрирует Boehm-Demers-Weiser GC; конкурентный, поколенческий GC запланирован на будущее.

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

fn process_audio_frame(frame AudioFrame) Dsp -> AudioFrame {
    realtime nogc {
        // здесь разрешено только размещение в стеке
        frame.apply_eq()
    }
}

Стандартная библиотека

core

Модуль core всегда в области видимости. Он предоставляет базовые типы (Option, Result, Vec, Map, Set, str, []u8), базовые протоколы (Eq, Ord, Hash, Display, Debug) и систему макросов.

io

Стандартный ввод, вывод и файловый ввод-вывод. Требует эффект Io. Включает stdin(), stdout(), stderr(), File.open(), File.create() и буферизованные чтение/запись.

net

TCP и UDP сокеты, разрешение DNS и TLS. Требует эффект Net. Все операции с сокетами совместимы с файберами — блокирующие вызовы прозрачно уступают управление планировщику.

collections

Расширенные структуры данных помимо core: BTreeMap, BTreeSet, LinkedList, Deque, PriorityQueue и неизменяемые (персистентные) варианты.

Стандартная библиотека активно разрабатывается. Многие модули существуют в скелетной форме. Вклад приветствуется — смотрите руководство для контрибьюторов.

Документация