Baga Programming Language
Spec-first systems language with effects as types, built for the age of AI.
What is Baga?
Baga (Бага) is a compiled, statically typed systems programming language that treats specifications and effects as first-class citizens. You write normal programs; the compiler keeps effects, specs, and proof sketches visible so a human — or an agent — can trust the result. It transpiles to C and compiles to native binaries with zero runtime dependencies. Identifiers can be written in both Latin and Cyrillic. Version 0.9.2.
The Three Pillars
Baga is built on three ideas that distinguish it from every other language:
Spec-First Verification
spec is a keyword. You write a specification first, then the implementation. The compiler checks implementations against their specs with --verify on any stated fragment.
Effects as Type Dimensions
str !IO !Net is a different type from str. Side effects show up in the type signature. Errors live in the type system, not in runtime surprises.
Readable Proof Sketches
The compiler emits human-readable sketches extracted from code and specs — not Coq or Lean proof objects. Certificates with honest UNKNOWN markers inside verified fragments.
Здравей, багатуре
A minimal Baga program. Every program must define a main function with no parameters. Execution starts there. Baga transpiles to clean C, then gcc produces a native executable with zero runtime dependencies. Cyrillic identifiers are fully supported.
Quick Start
The core compiler is a small C bootstrap — gcc and make only. An optional LLVM backend is available. The package manager sandak builds Baga packages from sandak.toml manifests. Product code lives in std/, app-product/, and apps/.
What is new in 0.9.2
The language arc now includes an opt-in RC memory model, generics and traits, effect payloads, and !Overflow as a type-level effect. On the product side, boilaDB 0.7 is a multimodal SQL server with NUMERIC, window functions, foreign keys, CHECK, SCRAM, COPY, and a Raft replica path — all written in Baga.
RC memory model
Optional --rc: ownership, containers, struct/enum fields, owned function results.
Generics & traits
Function and struct monomorphization, traits/impl, statically verified guarantees.
boilaDB 0.7
BoilaSQL + PostgreSQL wire :6575 + HTTP. NUMERIC, UNIQUE, FK, CHECK, windows, SCRAM, COPY.
Pure-Baga Cryptography
Cryptography is implemented in Baga — no OpenSSL/libcrypto at runtime. The TLS 1.3 client, HTTPS stack, and JWT signing/verification are written in pure Baga. OpenSSL is only a test peer.
Primitives
SHA-1/256, HMAC, AES, GCM, HKDF, bn, X25519, P-256/ECDSA, RSA (PKCS#1/PSS), DER, X.509
TLS 1.3 Client
Record layer, handshake, cert + CertificateVerify, application traffic — all in Baga
HTTPS
http:// and https:// over pure TLS — no external crypto dependencies
JWT
HS256 sign/verify; RS256/ES256 verify — OIDC-ready, cross-checked with Python goldens
Design Philosophy
The question is not "what is new". The question is "what has not been glued together yet". Specs, effects, and proofs are the foundation, not afterthoughts. The compiler is a small C bootstrap; the ecosystem is written in Baga itself. As in Rust, the package manager builds the packages, not the compiler.