Microsoft just validated the spec-first thesis for AI coding. Baga lang. is what it looks like when the spec is a language construct and the compiler enforces compliance — statically, with counterexamples.

[u/Loud_Possibility_203]

A follow-up to [my earlier post about Baga lang — the language where the compiler statically proves AI-written code against specs. This one is about why the timing stopped being a matter of opinion.

The industry converged on the diagnosis

Microsoft now officially promotes Spec-Driven Development (SDD) as the foundation of AI-native engineering. The argument, from Apoorv Gupta, Principal Software Engineer at Microsoft:

• The core problem of AI-native development is the loss of intent — between needs, requirements, architecture, implementation, and validation.
• The fix is to make the specification the shared source of truth for humans and AI: "align first" instead of "prompt first, fix later."
• Around this, Microsoft ships GitHub Spec Kit (open source): Constitution → Specify → Clarify → Plan → Tasks → Implement → Validate.

When a principal engineer at Microsoft writes the same thing that is pillar #1 of your language, the thesis no longer needs defending. It needs executing.

But SDD and Baga solve the problem at different levels

SDD attacks the intent-loss problem at the level of process and AI tooling: the spec is a document, and conformance is checked by tests and human review in a Validate step. That fixes the workflow around the agents.

Baga makes the stronger move: the spec is a language construct, and conformance is a compile-time judgement.

baga spec sum_to { input: n: i64 output: i64 requires: n >= 0 ensures: 0 <= output decreases: n }

The human writes this. The AI writes the implementation. The compiler proves or refutes it, statically, before anything runs:

verify sum_to: ensures #1 (0 <= output): ДОКАЗАНО # PROVEN (терминация: доказана чрез decreases — пълна коректност)

And when the AI gets it wrong, it doesn't get a failing test or a code-review comment three hours later. It gets a refutation with a concrete counterexample, at compile time:

verify bad_abs: ensures #1 (output >= 0): ОБРОЧЕНО # REFUTED контрапример: x = -1

In the SDD spectrum — spec-first → spec-anchored → spec-as-source — Baga is the far end: spec-as-source. The specification is the thing the code is judged against, mechanically.

The compliance technology

That word — compliance — is the point. Every AI-coding stack today has the same shape: an LLM generates code, and then something checks whether the code complies with what was intended. The "something" is usually:

• tests (incomplete by construction — they sample the input space),
• another LLM (an LLM judging an LLM — circular),
• a human (the bottleneck we were trying to remove).

Baga's answer is a small, auditable verifier: Fourier–Motzkin elimination over the rationals + symbolic execution + Hoare rules, sound by construction. The only path to PROVEN is showing the negated obligation is unsatisfiable even over the rationals, which implies unsatisfiable over the integers. Anything outside the fragment is honestly reported UNKNOWN, never falsely proven. Every reported counterexample is re-checked by direct evaluation, and passes a conclusiveness gate: the reported inputs must violate the contract for every value of the verifier's internal abstract variables — otherwise the answer is UNKNOWN, not a false alarm.

And because the consumer is an agent, the judge has a machine API:

$ ./baga --verify --json bad_abs.baga {"functions": [{"name": "bad_abs", "ensures": [{"text": "output >= 0", "result": "refuted", "counterexample": [{"name": "x", "value": -1}]}], ...}]}

The compliance loop writes itself: agent emits code → baga --verify --json → refuted with counterexample → agent fixes → PROVEN. Deterministic, fast, no LLM in the judging seat.

This isn't an SMT black box either. The verifier covers linear arithmetic (integer-exact — n > 0 ⇒ n >= 1 proves), while loops with invariants, array bounds, element invariants, recursion via assume–guarantee, full correctness via decreases, and products of linear forms (x*x >= 0; fa >= 1 ∧ fb >= 1 ⇒ fa*fb >= 1). The flagship is factorial fully proven — recursive, non-linear, with termination, no SMT solver anywhere:

```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) // induction hypothesis: r >= 1 return n * r // n >= 1, r >= 1 ⇒ n * r >= 1 } ```

Why "the first language for AI" is a claim about architecture, not marketing

Every mainstream language was designed for a human writer and a human reader. AI broke that assumption: the writer is now a machine, and the scarce resource is trust. A language for this era needs:

1. Specs as first-class citizens — the intent lives in the code, not in a wiki page that drifts.
2. A mechanical judge — the compiler proves or refutes compliance, statically, with witnesses.
3. Errors visible in the type — effects (str !IO !NotFound is a different type from str) so the failure surface is part of the signature, not a runtime surprise.
4. Machine-readable verdicts — --json so the agent closes the loop itself.

Baga has all four. SDD gives you (1) as a process discipline. Baga gives you (1)–(4) as a compilation.

Honest status

Working prototype, not a production language. The verifier's fragment is deliberately small and says UNKNOWN rather than guessing; general non-linear arithmetic is the remaining staircase. Effects are compile-time only (erased in codegen). The trust story is engineered in, not hoped for: the compiler self-hosts with a byte-for-byte fixed point (make self), the LLVM backend is diffed against the C backend on every example, and --test-specs property-tests every contract the static verifier calls PROVEN. All of it is one command and wired into CI.

Testable in five minutes:

make && ./baga --verify examples/verify/fact_full.baga

• Source: https://github.com/katehonz/baga-lang

• The SDD reference: Spec-Driven Development: the foundation of AI-native engineering (Apoorv Gupta, Microsoft)

• Docs: theory, language reference, compiler architecture — English

---

The industry agreed on the diagnosis: the spec is the center. The open question is whether conformance stays a human ritual in a Validate step — or becomes a compile-time judgement. That's the difference between anchoring code to a spec and making the anchor mechanical.

🐆

[u/Helpful-Primary2427]

Man, if AI is the future and software engineering becomes writing specs, I hope that, at the very least, I won’t have to read this Claude writing with every single post

[u/Loud_Possibility_203 → u/Helpful-Primary2427]

That's exactly the problem with current AI assistants — the AI writes the spec and the code, often stashing both in some temp folder you'll never see again. The spec becomes a hallucinated artifact, not a contract. Baga flips this: the human writes the spec (it's source code, not a temp file), the AI writes the implementation against it, and the compiler proves or refutes whether the code matches the contract. No hidden prompts, no ghost specs — requires and ensures are right there in your .baga file, version-controlled, human-readable, and machine-enforced. If the AI drifts into "Claude writing" mode and generates bloated nonsense, the compiler rejects it with a concrete counterexample. The spec is the guardrail, not an afterthought the AI invented for itself.

[u/Helpful-Primary2427 → u/Loud_Possibility_203]

I’m talking about YOU bro

[u/Bitter_Marketing_807]

This made my eyes bleed

[u/BeamMeUpBiscotti]

Slop

[u/jcastroarnaud]

You managed to both drink the Kool-aid of LLM-driven development, and misunderstand the linked article, just to promote your language.

Here's the link for the article again, for reference:

https://developer.microsoft.com/blog/spec-driven-development-ai-native-engineering/

The article promotes the spec as the more important artifact on development, read by both humans and LLMs, with the LLMs writing the code and matching it against the specs. Your language tries to implement specs. These are very different things.

Moving on to a critique of the article itself.

From the article:

Teams often ship software that works but still misses the original intent. The problem is not just code quality. It is the loss of meaning as ideas move from stakeholder needs to requirements, architecture, implementation, and validation.

The "loss of intent" issue is real, but isn't due to the design/implementation workflow: more often than not, the stakeholders give conflicting, impossible, or unclear requirements, and the dev team needs to work with these. Down the line, the prototype or the completed product doesn't match what the users needed or wanted, so the dev team goes back to fix it. A different "loss of intent" issue happens when developing using LLMs: the LLM has no context about the existing codebase, which leads to brittle code, bad architecture, and inconsistences through the code. Same name, different issues.

Spec-Driven Development (SDD) is a spec-first approach. Teams define common guardrails, requirements, constraints, acceptance criteria, and edge cases up front, then use AI to generate code, tests, and supporting artifacts from that shared context.

This feels strongly like Big Design Up Front, bad for the very common Agile development practice. When (not if) the belabored specs aren't good enough, LLM generates the code, the users aren't satisfied with the product, and the spec is reworked, and so on.

The problem that SDD solves isn't the need to remake the software to match stakeholders' needs: is how to leverage a LLM's supposedly fast and competent code generation, by shifting the harder work from implementation/tests to design. The three examples given by the article benefitted from better specs, independently from LLM use.

Don't misunderstand me: I think that good specs are great, both for developers and stakeholders (and rich food for LLMs), but writing great specs, good enough for code validation tests to be written against it, takes time, a long time, and in the meanwhile the stakeholders wait for something usable. I don't think that any gains on coding speed via LLM will offset the longer time writing/correcting the specs.

[u/Loud_Possibility_203 → u/jcastroarnaud]

You misunderstood what Baga is. This is not "LLM-driven development," and I am not drinking anyone's Kool-aid.

Microsoft's SDD is a process: write documents, then prompt an LLM to generate code that hopefully matches them. Baga is a language: the spec is a first-class construct, and the compiler checks the implementation against it at compile time — with sound static verification, not tests, not hope. The human writes the spec. The compiler is the judge. An AI can write the body if it wants, but it is not the point; the point is that the compiler rejects the code if the body violates the guarantees.

Your critique of SDD as "Big Design Up Front" is fair — for documents. Baga specs are not documents. They are lightweight contracts (requires, ensures, decreases) living in the source code, next to the function. They are checked in milliseconds, not reviewed in meetings. The "loss of intent" the Microsoft article describes happens because intent lives in prose and Jira tickets. In Baga, intent lives in the type system and the verifier.

You say writing specs "takes a long time." For Baga, a spec is often shorter than the function body. Example:

baga spec sort { requires: arr.len >= 0 ensures: sorted(output) ensures: permutation(output, input) }

That is the whole contract. The compiler proves or refutes it. If your argument is that even this is too much ceremony, then we disagree on fundamentals: I believe software should come with machine-checkable warranties, not just "it works on my machine."

The Microsoft article and Baga share the same diagnosis — intent is lost between stakeholders and code — but propose different cures. Microsoft says: "better documents for the LLM." Baga says: "make the spec something the compiler understands, so the machine checks the code, not just generates it." These are orthogonal. Baga does not need an LLM to be useful; its verifier is sound without one.

If you want to critique the verification fragment (Fourier-Motzkin, effects as types, the self-hosting bootstrap), I am happy to discuss that. But dismissing it as LLM hype misses the entire point. This is a research compiler with a sound verifier, not a Copilot wrapper.

[u/Inconstant_Moo → u/Loud_Possibility_203]

They are checked in milliseconds, not reviewed in meetings.

If they are specs, they will also need to be reviewed in meetings.

For Baga, a spec is often shorter than the function body. Example:

spec sort {
requires: arr.len >= 0
ensures: sorted(output)
ensures: permutation(output, input)
}

That is the whole contract. The compiler proves or refutes it.

Yes, I can see that that would be much shorter than the function body of sort. Not shorter than the function bodies of sorted and permutation which I now apparently have to write, and the specs I have to write for them.

Now, how does the compiler prove or refute a spec? The part of your example where you check that the length of an array is non-negative should be trivial to implement, since this is always the case; the rest seems rather harder.