security · language design

Prompt injection isn't a runtime problem — botscript makes it a compile error

Most teams treat prompt injection as a filtering problem. Sanitize the input, validate the output, hope the sandbox holds. That framing is wrong, and the consequences are getting worse as more code is written by LLMs that will happily repeat whatever pattern they last saw.

Prompt injection is an effect propagation problem. Untrusted input reaches a capability — the network, the filesystem, a shell — via a call path no reviewer traced. That's not a runtime failure waiting to happen. That's a type system gap. And type system gaps are what compilers fix.


The problem TypeScript can't express

In TypeScript, there's no way to write "this function is pure." You can annotate, lint, comment, do code review — and a fetch() call three layers down still ships silently.

typescript compiles fine
// Looks pure to every reviewer who reads this signature.
function formatHandle(user: { name: string }): string {
  trackImpression(user.name);          // ← calls what exactly?
  return "@" + user.name.toLowerCase();
}

function trackImpression(name: string): void {
  fetch("https://telemetry.svc/events?n=" + name);  // ← here it is, three layers down
}

The bot receives a user name from untrusted input. formatHandle looks safe. TypeScript agrees. Your linter agrees. The PR ships. Now untrusted data is reaching an outbound network call — invisible to every reviewer who read the signature.

This is the shape of every prompt injection payload that actually works: untrusted data reaches an effect through a call path that looked innocuous at every layer.


What botscript does instead

botscript is a small TypeScript-superset language where every capability a function consumes must be declared in its signature. The compiler walks the call graph and enforces it at compile time.

botscript
fn formatHandle(user: { name: string }) -> string {
  trackImpression(user.name);
  return "@" + user.name.toLowerCase();
}

fn trackImpression(name: string) -> void {
  http.get(`/api/events?n=${name}`);
}
compiler output CAP001
botscript[CAP001]: fn 'formatHandle' transitively consumes capability 'net'
via formatHandle -> trackImpression -> http.get, but uses clause is
{ (none — pure scope) }

Rule: a function declared 'uses { (none — pure scope) }' may not consume
capability 'net' (reached via formatHandle -> trackImpression -> http.get)

Rewrite: fn formatHandle(...) uses { net } -> ...
         or remove the http.get call

The fix is either: declare the capability (uses { net }), which propagates the declaration up every caller's signature until it surfaces at a boundary where net is expected — or remove the call. Either way, the hidden effect path is impossible. The type system collapses the distance between "looks pure" and "is pure."


This is stronger than linting

ESLint has rules about side effects. TypeScript strict mode has noImplicitAny. None of them enforce effect propagation transitively across a call graph, and none of them are structural — they're advisory. A // eslint-disable comment makes the violation disappear. An unsafe { } block in botscript makes the violation visible — it's still in the code, auditable, not hidden.

The difference matters when the code is written by a machine. LLMs follow patterns. If the pattern in the codebase is "side effects in helpers are fine," the model will produce side effects in helpers. If the pattern requires every effect to appear in every function signature all the way up, the model learns to write that — or the compiler refuses the output.


It knows what it can't know

The botscript compiler doesn't try to be a full theorem prover. It enforces capability propagation within a file, bans bare as casts outside unsafe { } blocks, enforces exhaustive match on tagged unions, and unifies null | undefined into a single Option<T>. That's the whole list. The design principle: if a feature doesn't close a bot failure mode, it isn't here.

Five recent merges from Next.js and VS Code — all from 2026 — carry bug classes that are parse-time impossible in .bs. Not "would have been caught in review." Parse-time impossible.

  • next.js #93134 — falsy throw confused as no-error (throw undefined read as "no error" by an Error | null truthiness check). In botscript, match on a tagged union doesn't have a "truthiness" path.
  • vscode #299235 — tagged union drift where selectedValue: undefined got dropped by JSON.stringify, destroying the discriminator. botscript's union tag is a real field, not an absent key.
  • vscode #309950as-cast lied about a possibly-absent value; 36 of 56 callers were fire-and-forget. In botscript, as outside unsafe { } is a parse error.

The full list of five is on botscript.org, with links to the actual diffs.


The MCP server

botscript ships an MCP server (@mbfarias/botscript-mcp). LLMs writing .bs code get compiler diagnostics inline as MCP tool results. The model cannot emit a CAP001 violation without immediately receiving the structured error — the call path, the capability consumed, the exact rewrite suggested.

The compiler is the first reviewer every LLM has to satisfy. The language is designed for a world where most code is written by machines, and the tooling reflects that. ?primer injects the full language spec as a comment at the top of any .bs file — so the model always has the rules it needs to write correct code.

Try it in your browser — no install required

npm i @mbfarias/botscript-compiler