Введение

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

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

Установка

Самый быстрый способ начать — скрипт установки:

curl -sSf https://nv-lang.org/install.sh | sh

Это устанавливает компилятор nova и пакетный менеджер nv в ~/.nova/bin. Добавьте эту директорию в PATH:

export PATH="$HOME/.nova/bin:$PATH"

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

Системные требования: Linux x86-64 или ARM64, macOS 12+. Поддержка Windows запланирована.

Hello, World

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

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

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

nova build hello.nv
./hello

Обратите внимание, что main объявляет Io перед стрелкой возврата — даже точка входа верхнего уровня честна в отношении своих эффектов. () — тип возврата unit (значение не возвращается).

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

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

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

Эффекты

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

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

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

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

// Эффекты 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-решатель на этапе компиляции — доказанные стираются в release без затрат в runtime. Если солвер не может принять решение, контракт автоматически откатывается до runtime-assert'а в debug-сборках. Атрибут #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
Алгебраические типы: struct для произведений, enum для помеченных объединений
Option и Result: Option[T] и Result[T, E] — встроенные перечисления, никакого null
Дженерики: параметрический полиморфизм с ограничениями протоколов
Протоколы: структурные интерфейсы с реализациями по умолчанию

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

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

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

// spawn для fire-and-forget работы; 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 и персистентные/иммутабельные варианты.

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

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