Bosque

Bosque is a language built around a single, deliberately provocative claim: that the for loop is to 2019 what GOTO was to 1968. Mark Marron’s argument, made in the Microsoft Research technical report that introduced the language, is that structured programming succeeded not because while is more expressive than a jump — it is strictly less expressive — but because constraining control flow made programs comprehensible to humans and analyzable by machines. Bosque proposes the next constraint: get rid of the loop itself, along with mutable state, aliasing, reference equality, and everything else that forces a compiler or a verifier to reason about when something happened rather than what it means.

The result looks, at a glance, like ordinary TypeScript. It has curly braces, function, return, type annotations after colons. Underneath, it behaves like ML: everything is a value, evaluation is deterministic, and iteration happens through algebraic bulk operations over collections rather than through an index that mutates until a condition flips. Marron’s term for this is regularized programming — removing the irregular corners of language semantics so that both a human reading the code and a tool analyzing it arrive at the same, single answer about what it does.

History and Origins

Bosque came out of Microsoft Research, where Marron spent roughly a decade before moving into academia. The GitHub repository was created in March 2019; the technical report, MSR-TR-2019-10, is dated April 2019; and the public announcement in mid-April produced an unusually large wave of press for a research language — The Register on 18 April, then Slashdot, DZone and a long tail of blog coverage. The framing that travelled best was “the language with no loops,” which is accurate but was widely read as a gimmick rather than as the load-bearing design decision it actually is.

The motivating observation is about tooling economics. Automated program reasoning — verification, symbolic execution, test generation, sound refactoring, precise resource analysis — is hard on mainstream languages not because the ideas are missing but because the languages are hostile. Two variables may or may not alias. A loop may or may not terminate. An object’s identity may matter, or only its contents may. x may have been mutated by a callee. Every one of these possibilities multiplies the state space a tool must consider, and most of them exist because of choices made in the 1970s for reasons that no longer apply.

Marron’s bet was that if you designed the language so those questions could not be asked, the tools would suddenly become tractable — and that the expressive power you gave up would turn out to be less than programmers assume. The Microsoft Research project page describes the work as investigating a code intermediate representation that enables deep automated reasoning, then building a developer-accessible language on top of it, with a cloud-first perspective on microservice and serverless deployment.

In October 2022 the project moved. A new repository, BosqueLanguage/BosqueCore, was created outside the microsoft organization; the original microsoft/BosqueLanguage received its last commit that same month and was eventually archived read-only, sitting at roughly 5,200 stars — most of them, in all likelihood, accumulated during the 2019 news cycle. Marron joined the University of Kentucky as faculty, reportedly in January 2024, and Bosque became his group’s principal project. The star count on BosqueCore is a couple of hundred, which is a fair measure of the difference between attention and use.

Design Philosophy

Regularization over expressiveness. The organizing principle is that every semantic irregularity in a language is a tax paid by every reader and every tool, forever. Bosque removes constructs whose only justification is history. The measure of a feature is not whether it is occasionally convenient, but whether its absence makes anything genuinely harder to express.

No spooky action at a distance. The BosqueCore documentation states this as a first-class goal: a piece of Bosque code should be understandable in isolation, and its behavior must not depend on the context it runs in or on implicit ambient effects. This is what falls out of removing mutable aliasing — if a callee cannot reach and modify your data, reading the callee’s signature tells you what it can do.

Determinism as a language guarantee, not a testing aspiration. Core Bosque is fully deterministic: for a given input there is exactly one possible output. Nondeterministic interaction with the outside world — I/O, time, randomness, concurrency — is not forbidden, but it is confined to explicit Task environments rather than being available anywhere a function body can reach. Reproducing a field failure becomes a matter of replaying recorded inputs rather than recreating a race.

Poke-yoke programming. The Japanese manufacturing term for a design that makes the wrong assembly physically impossible is the project’s preferred description of its safety posture. Full memory safety, loop-free iteration, typed strings and type invariants are meant to combine so that the obvious way to write something is also the correct way. The project claims that of the 2024 MITRE Top-10 CWE categories, three are impossible in Bosque and five more require explicitly opting out of a safety feature — a project claim about its own design, not an independent audit.

Simplicity in the language buys simplicity in the runtime. Because the compiler knows tightly what any given piece of code can do, the runtime can make guarantees that a general-purpose one cannot. The project states that this enabled what it describes as the first no-tradeoff garbage collector, with bounded pauses, starvation freedom, and bounded CPU and memory overhead simultaneously. That is a strong claim and should be read as the project’s own characterization of its collector’s design goals rather than as an independently benchmarked result; published measurement details are limited.

Key Features

Functions and typed literals. Bosque syntax is TypeScript-shaped, but numeric literals carry type suffixes and there is no implicit numeric conversion:

public function sub2(x: Int, y: Int): Int {
    return x - y;
}

sub2(4i, 2i)     %% 2i
sub2(y=2i, x=3i) %% 1i — named arguments

sub2(3i, 4.0f)   %% type error: Float given where Int expected
sub2(3, 4)       %% type error: un-annotated numeric literals are not supported

%% is a comment. The i, n and f suffixes mark Int, Nat and Float — the language would rather make you say which numeric type you mean than pick one and quietly widen it later.

Loop-free iteration. There is no for and no while. Iteration is expressed with algebraic operations over collections, which is where the “no loops” headline comes from:

public function allPositive(...args: List<Int>): Bool {
    return args.allOf(pred(x) => x >= 0i);
}

allPositive(1i, 3i, 4i)  %% true
allPositive()            %% true
allPositive(1i, 3i, -4i) %% false

The practical consequence is that off-by-one errors, iterator invalidation and unbounded loops are not bugs you can write. The analytical consequence is more important: a bulk operation has a known shape, so a verifier can reason about it directly instead of searching for a loop invariant.

Functional state updates with an imperative feel. Immutability is the default, but Bosque is unwilling to make the programmer thread state manually through every call. Both styles are supported, and the second desugars to the first:

%% Manual threading of state
entity Ctr {
    field vv: Nat = 0n;
    method next(): Ctr {
        return Ctr{ vv = this.vv + 1n };
    }
}

let ctr = Ctr{};
let ctr1 = ctr.next();
let ctr2 = ctr1.next();
ctr2.vv; %% 2n

%% Reference parameters and updates — still functional underneath
entity Ctr {
    field vv: Nat = 0n;
    ref method next() {
        ref this[vv = $vv + 1n];
    }
}

ref ctr = Ctr{};
ref ctr.next();
ref ctr.next();

The ref mode is a controlled, non-aliasing update path: the caller explicitly marks the variable being rebound at the call site, so the “spooky action” that ordinary mutable references permit is still ruled out.

Typed strings. A String is a bag of characters; a typed string carries the grammar of what it holds, so a validated email address, a SQL fragment and a filesystem path are different types. This is the direct answer to the injection-flaw families in the CWE lists — you cannot pass an unvalidated string where a validated one is required, because they do not unify.

Type invariants. Entities can declare invariants over their fields that the runtime enforces at construction, which means a value of a given type is, by construction, a value satisfying that type’s stated constraints. Combined with pre- and post-conditions, these are exactly the properties the planned small-model verifier is designed to discharge.

Explicitly encapsulated effects. Task environments carry the nondeterministic parts of the world — I/O, scheduling, external services. Core computation stays pure, which is what makes deterministic replay and distributed tracing feasible as language features rather than as instrumentation bolted on afterward.

Evolution

The most consequential event in that table is the 2022 restart. The 2019 implementation was a prototype written in TypeScript and run on Node.js — appropriate for demonstrating that a design is coherent, and unsuitable for anything else. BosqueCore is the second system, and the roadmap items that go with it (native compilation, a purpose-built garbage collector, async task runtime, an LSP server, a symbolic verifier) describe an attempt to build the real thing rather than another prototype.

The 2.0 announcement is worth reading carefully. It does not claim the language is finished; it claims the design has stopped moving and the work is now about libraries, tooling and users. That is a normal and honest thing for a seven-year-old research project to say. It is also unaccompanied by tagged releases, versioned binaries or a package registry, so “2.0” describes a stated project milestone rather than a distributed artifact you can pin a dependency to.

Current Relevance

Bosque is active but small. Commits were still landing on BosqueCore at the end of July 2026, the contributor list is a handful of people centered on Marron’s research group, and the roadmap is explicit that core libraries, LSP support and the verifier are all still in progress. The stated goal is now to get Bosque deployed in the real world and fix what breaks — a reasonable ambition, and one that no research language achieves by default.

What it is genuinely useful for today:

• Studying language design under a verification constraint. Most languages add analysis tooling afterward and discover which features made it impossible. Bosque inverted the order, and reading it is the fastest way to see what that costs and what it buys.
• Understanding the loop-free argument on its merits. Once you have written a few Bosque functions, the claim that explicit iteration is mostly ceremony stops sounding like a stunt. The same argument has quietly won in other places: LINQ, Rust iterator chains, Java streams, array languages, and every dataframe API in existence.
• Prior art for correct-by-construction and AI-assisted development. The 2.0 roadmap treats AI agents and APIs as first-class parts of the stack, on the theory that a deterministic, aliasing-free, invariant-checked language is a better target for machine-generated code than one where a plausible-looking program can be subtly wrong. Whether or not Bosque itself is the vehicle, that argument is now everywhere.

What it is not: production-ready, ecosystem-equipped, or a safe technology choice for shipping software. There is no package manager, no substantial standard library relative to mainstream expectations, no stable toolchain distribution, and no track record of anyone running it in anger. Platform support is narrow and stated only as build prerequisites rather than as a support matrix: the BosqueCore README lists a 64-bit Linux operating system (Ubuntu 24 recommended), Node.js 22 or later, TypeScript 5.6 and Git, with the compiler transpiling Bosque sources to C++ and a Makefile that you then build. No other platform is documented as supported, and anyone evaluating the language should check the current build instructions in the repository rather than assume otherwise, since the implementation has changed substantially since 2019.

Why It Matters

Bosque’s importance is almost entirely about the argument, not the adoption — which is the normal condition for research languages, and not a criticism.

The argument is that programming language design has been optimizing for the wrong reader. For fifty years, features have been justified by what they let a human express, with analyzability treated as a downstream tooling problem. Bosque asks what happens if you invert that: design for the machine that has to reason about the program, and see whether humans mind. Marron’s structured-programming analogy is the strongest form of the case. Dijkstra’s argument against GOTO was, at the time, an argument for giving up power, and it was resisted on exactly those grounds. It won because comprehensibility compounds and raw expressiveness does not.

Three specific bets Bosque made in 2019 look better in 2026 than they did at the time. Immutability by default has continued its march from functional languages into the mainstream. Effects as an explicit, encapsulated thing rather than an ambient capability is now visible in effect systems, capability-based designs and structured concurrency across a dozen languages. And designing for machine-generated code — the idea that a language should make it hard for a generator to produce a plausible-looking wrong program — was a fringe concern in 2019 and is a central one now.

There is also a lesson in the shape of Bosque’s public life. It arrived with an enormous press wave, collected five thousand stars in a few weeks on the strength of one headline about loops, and then did the actual work in near-total obscurity for the next seven years with a couple of hundred people watching. The attention had almost nothing to do with the research and did almost nothing for it. The language is more interesting now, with a second implementation and a coherent roadmap, than it was on the day everybody wrote about it.

Whether Bosque itself gets used is an open question, and the honest answer is that most languages in its position do not. But the constraint it was built to test — that a language should be designed so tools can prove things about it — is one the industry is converging on from several directions at once. Bosque is the version of that idea that refused to compromise, which makes it the clearest place to see both what the idea is worth and what it costs.