Baga 0.8.4 Released — Effects, Specs, and Pure Crypto
2026-08-11 16:26:20
Baga 0.8.4 is now available. This release solidifies the three pillars of the language: spec-first verification, effects as type dimensions, and readable proof sketches.
The effect system (!IO, !Net, !Par, !NotFound) is now stable. Functions declare their side effects in their type signature, and the compiler enforces effect correctness across the entire call graph. Pure functions cannot accidentally call effectful ones.
Spec verification (--verify) now produces certificates with honest UNKNOWN markers for unproven fragments. The spec system supports input/output declarations, guarantees (human-readable properties), and ensures (machine-checked constraints).
The pure-Baga cryptography stack is a highlight: TLS 1.3 client, HTTPS, and JWT are all implemented in Baga without linking against OpenSSL at runtime. OpenSSL is only used as a test peer for validation.
Package manager sandak now resolves local path dependencies, git dependencies, and registry packages. Each package has a sandak.toml manifest, and the build graph is resolved deterministically.
Quick start: git clone, make, ./baga examples/zdravei.baga — that is all you need. Zero dependencies beyond gcc and make.
The effect system (!IO, !Net, !Par, !NotFound) is now stable. Functions declare their side effects in their type signature, and the compiler enforces effect correctness across the entire call graph. Pure functions cannot accidentally call effectful ones.
Spec verification (--verify) now produces certificates with honest UNKNOWN markers for unproven fragments. The spec system supports input/output declarations, guarantees (human-readable properties), and ensures (machine-checked constraints).
The pure-Baga cryptography stack is a highlight: TLS 1.3 client, HTTPS, and JWT are all implemented in Baga without linking against OpenSSL at runtime. OpenSSL is only used as a test peer for validation.
Package manager sandak now resolves local path dependencies, git dependencies, and registry packages. Each package has a sandak.toml manifest, and the build graph is resolved deterministically.
Quick start: git clone, make, ./baga examples/zdravei.baga — that is all you need. Zero dependencies beyond gcc and make.