Язык программирования Baga
Системный язык со spec-first верификацией и эффектами как типами — для эпохи ИИ.
Что такое Baga?
Baga (Бага) — компилируемый статически типизированный системный язык, в котором спецификации и эффекты — полноценные граждане. Вы пишете обычные программы; компилятор держит эффекты, спецификации и proof sketches на виду, чтобы человек — или агент — мог доверять результату. Транспилируется в C и собирается в native binary без runtime-зависимостей. Идентификаторы — и латиницей, и кириллицей. Версия 0.9.2.
Три столпа
Baga стоит на трёх идеях, которые отличают его от любого другого языка:
Spec-first верификация
spec — ключевое слово. Сначала спецификация, потом реализация. Компилятор проверяет её через --verify на заявленном фрагменте.
Эффекты как измерения типов
str !IO !Net — другой тип, нежели str. Побочные эффекты видны в сигнатуре. Ошибки живут в системе типов, а не в сюрпризах runtime.
Читаемые proof sketches
Компилятор извлекает читаемые наброски из кода и спецификаций — не proof objects как в Coq или Lean. Сертификаты с честным UNKNOWN внутри проверенного фрагмента.
Здравей, багатуре
Минимальная программа на Baga. У каждой программы есть main без параметров. Исполнение начинается там. Baga транспилирует в чистый C, gcc даёт native исполняемый файл без runtime-зависимостей. Кириллические идентификаторы поддерживаются полностью.
Быстрый старт
Ядро компилятора — небольшой C bootstrap: только gcc и make. Опционален LLVM-бэкенд. Менеджер пакетов sandak собирает пакеты Baga по манифестам sandak.toml. Продуктовый код — в std/, app-product/ и apps/.
Что нового в 0.9.2
В языковой дуге теперь опциональная RC-модель памяти, дженерики и трейты, payload эффектов и !Overflow как типовой эффект. Со стороны продуктов boilaDB 0.7 — мультимодальный SQL-сервер с NUMERIC, оконными функциями, внешними ключами, CHECK, SCRAM, COPY и Raft-репликой. Всё написано на Baga.
RC-модель памяти
Опциональный --rc: владение, контейнеры, поля struct/enum, возвращаемые owned-значения.
Дженерики и трейты
Мономорфизация функций и структур, traits/impl, статически проверенные guarantees.
boilaDB 0.7
BoilaSQL + PostgreSQL wire :6575 + HTTP. NUMERIC, UNIQUE, FK, CHECK, окна, SCRAM, COPY.
Криптография на чистом Baga
Криптография реализована на Baga — без OpenSSL/libcrypto в runtime. TLS 1.3 клиент, HTTPS-стек и подпись/проверка JWT — чистый Baga. OpenSSL только тестовый сосед.
Примитивы
SHA-1/256, HMAC, AES, GCM, HKDF, bn, X25519, P-256/ECDSA, RSA (PKCS#1/PSS), DER, X.509
TLS 1.3 клиент
Record-слой, handshake, сертификат + CertificateVerify, прикладной трафик — всё на Baga
HTTPS
http:// и https:// поверх чистого TLS — без внешних криптозависимостей
JWT
HS256 подпись/проверка; RS256/ES256 проверка — готов к OIDC, сверено с Python goldens
Философия дизайна
Вопрос не в том, «что нового». Вопрос в том, «что ещё не склеено вместе». Спецификации, эффекты и доказательства — фундамент, а не послесловие. Компилятор — маленький C bootstrap; экосистема написана на самом Baga. Как в Rust: пакетный менеджер собирает пакеты, а не компилятор.