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 1.1.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 1.1.2
Baga 1.0 landed, then 1.1.2 extended the verifier, the TLS stack, and the product layer. --verify now reasons about structured concurrency liveness (M19–M30). Cryptography includes a TLS 1.3 server. boilaDB muxes PG and HTTP connections. bagabuch and chronobaga join the ecosystem.
Wait-for verification
M19–M30: deadlock on join-before-send, send on a full buffer, nested go, server loops. Deadlocks are REFUTED; outside the fragment is UNKNOWN.
>>> and TLS 1.3 server
Logical right shift (zero-fill). Pure-Baga TLS 1.3 server handshake; boilaDB and pgbaga speak TLS on the PG wire.
boilaDB mux + bagabuch
Connection mux, ~109k tps pgbench -S at c=16. bagabuch: Bulgarian accounting. chronobaga: civil dates.
Pure-Baga Cryptography
Cryptography is implemented in Baga — no OpenSSL/libcrypto at runtime. The TLS 1.3 client and server, 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, PEM private keys
TLS 1.3
Client and server handshake, record layer, CertificateVerify, application records chunked to 16 KB — 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.