Програмен език Baga
Системен език със spec-first верификация и ефекти като типове — за ерата на AI.
Какво е 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: мениджърът на пакети строи пакетите, не компилаторът.