Baga programing lang. Новата собствена софтуерна технология на cyberbuch

Baga  programing lang.  Новата собствена  софтуерна  технология на cyberbuch

Между Rust и чистия C? Не съвсем — и това не е най-интересното за Бага


Хората, които за пръв път видят Baga , почти винаги казват едно и също: *„това е нещо между Rust и чист C"*. Разбирам откъде идва. Синтаксисът изглежда съвременен като Rust, а под капака има C bootstrap, транспилиране към C и нула зависимости — като чист C. Но сравнението е хем вярно на повърхността, хем подвеждащо точно там, където езикът е най-интересен. Нека разгледам честно и двете половини.


Между Rust и C" описва ергономията и паметта. Но залогът на Бага е другаде — и той не е „между" нищо.* https://github.com/katehonz/baga-lang

## Къде сравнението е вярно

Първо, честно към критиците: в няколко оси Бага наистина седи между двата полюса.

**Ергономията е рустоподобна.** `fn`, `let`/`let mut`, `match`, структури, изброими типове, `Vec<T>`, интерполация на низове — всичко това е модерно и удобно, без да е тежко. Пишеш и виждаш изразителен език, не асемблер с шевове. В това отношение Бага е далеч по-близо до Rust, отколкото до C.

**Инструментариумът е чист C.** Основният компилатор е C bootstrap с **нула зависимости** — само `gcc` и `make`. Изходът е C. Самокомпилира се до неподвижна точка (`baga2 == baga3`, байт по байт). Това е дисциплината и простотата на C — нещо, което Rust умишлено захвърли в полза на LLVM-монолит и borrow checker.

**Паметта е… по средата, но не както си мислите.** Тук е първата пукнатина в сравнението. Rust няма еквивалент в Бага — **няма borrow checker**. Няма да се борите с компилатора за времена на живот. Но има opt-in **RC модел на паметта** (`--rc`): собственост, контейнери, полета в структури и енуми, върнати резултати. Тоест Бага не е „безопасен като Rust по подразбиране", а „прост като C по подразбиране, с предпазен колан, ако го поискаш". Това не е полусфера между двата свята — това е съзнателен избор да не повтаряш най-голямата цена на Rust.


Дотук — да, „между Rust и C" работи като груба карта. Но картата свършва точно там, където започва истинският залог.

## Къде сравнението пропуска целия смисъл

Rust зададе въпроса на 2015-а: **„как да предотвратим segfault-ове?"** Бага задава друг въпрос — този на 2026-а: **„как да се доверим на код, който не сме писали?"**

Това не е разлика в градус. Това е разлика в ос.

**Rust няма нищо, което да отговаря на спецификациите на Бага.** В Бага спецификацията е езикова конструкция и компилаторът **доказва или оборва** имплементацията спрямо нея — статично, преди да се изпълни ред:


```baga

spec fact {

input: n: i64

output: i64

requires: n >= 0

ensures: output >= 1

decreases: n

}


fn fact(n: i64) -> i64 {

if n <= 0 { return 1 }

let r = fact(n - 1) // индукционна хипотеза: r >= 1

return n * r

}

```


```bash

$ ./baga --verify fact.baga

verify fact:

ensures #1 (output >= 1): ДОКАЗАНО

(терминация: доказана чрез decreases — пълна коректност)

```


Rust ще ви провери типовете и паметта. Няма да ви каже — с **контрапример**, ако сгрешите — че функцията ви връща нещо извън договореното. Това не е върху оста Rust↔C. Това е територия на Dafny, Whiley, Liquid Haskell — но с малък, проверим двигател (елиминация на Фурие–Моцкин + символно изпълнение + правила на Хоар) вместо черна кутия със SMT солвер.


**Rust няма ефектна система.** В Бага `str !IO !Net` е **различен тип** от `str`. Необработен ефект е грешка по време на компилация, не изключение по време на изпълнение:


```baga

fn read_file(path: str) -> str !IO !NotFound {

let handle = open(path)?

read(handle)?

}


fn main() {

let content = read_file("data.txt")

catch !NotFound => "empty"

catch !IO => "error"

print(content)

}

```


Това е Plotkin & Power (2003), направено практично — територията на Koka и Unison. Rust няма нищо подобно; `Result<T, E>` е библиотечен шаблон, не измерение на типа.


**Rust не извлича доказателства.** `--proofs` вади четим текст — `theorem fact_terminates`, `theorem fact_pure` — от самия код. Това е **обратното** на Coq: Coq извлича програми от доказателства, Бага извлича доказателствени скици от програми.


Ето защо „между Rust и чист C" е подвеждащо. То описва **ергономията** и **паметта**, но мълчи за трите стълба, заради които езикът съществува. Все едно да опишете Lisp като „синтаксис със скоби" — вярно, но пропускате въпроса, който Lisp задава.


## Какво е Бага всъщност?

Ако трябва да го сложа на картата честно, бих казал така:

- **Като C** — по дух на простота и по инструментариум (zero-dep bootstrap, транспилиране към C, самокомпилация до неподвижна точка).

- **Като Rust** — по ергономия и по амбиция за коректност (но без borrow checker; вместо него — opt-in RC).

- **Като Koka/Dafny/Whiley** — по ефектната система и статичната верификация, но с малък, одитируем верификатор, който казва НЕИЗВЕСТНО вместо да гадае.

Иначе казано: **синтаксисът е между Rust и C, но тезата е отвъд и двете.** Тезата е, че в ерата на AI пишещия код дефицитният ресурс вече не е безопасността на паметта (Rust я спечели през 2015-а) и не е суровата скорост (C я има от 1972-а) — дефицитният ресурс е **доверието**. Доверие в код, който не си писал ти, а е излъчил агент. Ако Rust е отговорът на „кой ще пази паметта", Бага се опитва да бъде отговорът на „кой ще пази смисъла".


## Моето мнение — без захар

Понеже ме питате честно, ето го честно.

**Най-силното нещо в Бага не е езикът сам по себе си, а вертикалът.** Език не се доказва с тези — доказва се като компилаторът компилира сам себе си до неподвижна точка, базата данни (`boilaDB`) говори протокола на PostgreSQL с истински `psql`, а най-отгоре стои счетоводна програма (`bagabuch`), която издава фактури с ДДС по ред и генерира SAF-T за НАП. Този вертикал — [от самокомпилатора до първата фактура](ekosistema-baga-bg.md) — е рядък, и той е истинският тест на езика, не демотата.

**Най-интересната идея е „спецификацията като присъда, не като коментар".** Microsoft вече промотира Spec-Driven Development като *процес*. Бага прави по-силния ход: спецификацията е *езикова конструкция*, а съответствието е *присъда по време на компилация*. Това е единствената посока, в която AI-нативното инженерство може да не завърши с „LLM съди LLM".


**Честните слабости.** Това е работен прототип, не производствен език. Фрагментът на верификатора е умишлено малък — общата нелинейна аритметика (полиноми от по-висока степен, деление с променливи) е оставащото стълбище. Ефектите са само по време на компилация. Няма borrow checker — което е и освобождение, и празнина за тези, които търсят Rust-гаранции по подразбиране. И най-вече: език без общност е граматика; Бага е все още на етапа, в който трябва да убеди първата кохорта, че залогът е реален, а не още една рекомбинация на стари идеи.


**Присъдата ми.** „Между Rust и чист C" е удобно свиване, но несправедливо. То поставя Бага на ос, която той съзнателно не играе — ос на памет и ергономия — и скрива оста, която го прави различен: доверието в код от AI. Ако през 2026-а искате просто още един системен език, Бага няма да ви спечели. Ако искате да видите какво става, когато компилаторът спре да бъде проверяващ типове и стане **съдия, който доказва** — тогава си струва да следите точно този език, а не етикета, който му лепват.


*Нищо не е ново. Линейната логика е от 1987-а — отне ѝ 30 години да стане Rust. Ефектните системи са от 2003-а. Може би сега им е времето — а въпросът вече не е „какво е ново", а „какво още не е слепено заедно".*


⚔️ https://github.com/katehonz/baga-lang

Сподели