Martin Odersky opened Scala Days 2026 with a question he admits he can’t answer: if agents write the code and other agents review it, what are humans and programming languages still for? He doesn’t predict the future. He argues about which one we should want, and then shows a working piece of it. His group’s agent harness, which uses Scala 3’s capture checking to stop an agent from leaking secrets at compile time, won a best paper award at an ACM agentic-systems conference this spring. The second half of the keynote proposes three language features for keeping people in control of large programs that agents mostly write.

The program becomes a black box

Slide: Typical workflow, where the program itself is a black box

The workflow most teams are drifting toward goes like this: a human writes a prompt, the agent produces a program, users file tickets, and the tickets go back into the agent. Nobody looks inside. If that’s where things end up, language design stops mattering. Whatever is cheapest in tokens and fastest to iterate wins, and readability, modularity and safety stop being anyone’s concern.

Odersky’s objection is about agency, not jobs. If people give up the ability to understand and review software, he says, they “literally hand the keys to the agents, our own or an attacker’s.” The usual answer is to raise the level of abstraction the way compilers did, so that nobody needs to read assembly any more. That analogy breaks because agents are “flaky compilers”: the same input gives different outputs and there’s no guarantee about what they produce. Asking the model nicely won’t fix that, and neither will waiting for the next model. Control has to come from outside the model.

Agents already run unreviewed code

Slide: How to contain AI agents? Current defenses fall short

Tool-calling agents are the extreme case. They generate small programs that execute immediately with real side effects, and no human reads them. Odersky goes through the current defences and finds each one too coarse. Allow and block lists end up either too permissive or too strict. Confirmation prompts don’t scale because people stop reading them. Sandboxes grant one fixed set of permissions for the whole session.

His example of what none of them catch: an agent reads a secret in step one and exfiltrates it in step five, and each step looks fine on its own. Banning secret reads or banning all outbound traffic would stop it, but it would also stop most useful work. What’s needed is information-flow tracking. That’s also the only proper fix for Simon Willison’s “lethal trifecta” of private data, untrusted content and external communication, because in practice you can rarely take any one of the three away from an agent.

Make the medium safe

Slide: The key idea. Don’t try to make the model trustworthy. Make the medium safe.

“We don’t try to make the model trustworthy… We try to make the medium safe.”

Instead of letting agents emit arbitrary tool calls, the agent writes its intent as code in a capability-safe language (Scala 3 with capture checking). The compiler type-checks it, and only code that passes gets executed. The compiler does the enforcing, not the model.

The idea underneath is the capability: an unforgeable token that grants permission to do something, which you can pass on but can’t create yourself. What’s new is tracking capabilities in types. A plain String or an Int -> Int function is pure. File^{io} or Int ->{io} Int declares that the value holds an IO capability. Int => Int means “might hold anything.” Odersky notes that Scala kept the single arrow unused for years, waiting until it could mean purity.

Slide: Key concept, tracked capabilities

Classified data and the dual LLM pattern

Slide: Capabilities for agents, the Classified[T] protocol

Private data gets wrapped in Classified[T]. Unwrapping it with reveal requires a CanAccess[T] capability, which the agent never receives. What the agent can do is map over classified values with a pure function and combine classified values together. A pure function holds no capabilities, so inside the transform the agent can’t print, write to the network or stash the value in a variable. When the transform finishes, the agent knows nothing it could leak later. Odersky is upfront that timing channels (taking 100 seconds rather than one to signal a bit) aren’t covered. The same mechanism extends to multiple security levels and to marking untrusted input, which handles indirect prompt injection.

This gives the dual LLM pattern something to enforce it. There are two overloads of chat. The one that takes a plain string goes to a cloud model. The one that takes a Classified[String] returns a Classified[String] and is routed to a local trusted model. Overload resolution picks the right model based on the data’s type, so private data can’t reach the public one.

TACIT, and what the compiler catches

Slide: What the compiler catches, real examples

The harness is called TACIT (tracked agent capabilities in types). The agent sends Scala snippets to an MCP server, which compiles them against a capability-annotated library and then runs them in a REPL. A “safe mode” language import turns off the escape hatches for agent code: no unchecked casts, no caps.unsafe, no runtime reflection. Trusted library code that eventually calls into Java is marked @assumeSafe and has to be audited, in roughly the way Rust treats unsafe blocks.

The slide’s examples come from real benchmark runs. An agent that tries to println a classified API key inside map gets a type error: the compiler found String ->{io} Unit where it needed String -> Unit. An agent that tries to return file handles out of a scoped file-system request gets “capability outlives its scope.” On standard agent benchmarks, including AgentDojo and SWE-bench, the team found the approach both blocks unsafe behaviour under adversarial conditions and keeps agents as effective as with conventional tool calling. The paper is Securing Agents with Tracked Capabilities.

From agent snippets to million-line programs

Agents and large codebases share one goal, which is trusting the system without reading every line, and strong types help with both. The differences are scale and lifespan. Agent snippets live for minutes and run to ten lines. Programs live for decades, run to millions of lines, and can be partly reviewed. Odersky also quotes Kent Beck’s complaint that agent work feels like being an air traffic controller rather than working in flow, and calls that a practical loss as well as an emotional one.

Slide: Some ideas. Strong types, spec strings, required interfaces, refinement types

He offers three tentative ideas on top of strong types and says plainly that they’re meant to start a discussion.

Spec strings. The prompt stays in the source file next to the code it produced. A change request edits the spec, and the agent’s job is to keep the code in sync with it. Reviewing a function then means reading its spec and its signature, while the types limit what the implementation could possibly do.

Required interfaces. Today only library authors declare interfaces. Odersky wants consumers to declare what they need from a dependency too, including which global capabilities it may use. In his supply-chain example, a JSON parser that uses Console is changed by an attacker to uses Console, Network and asks for an implicit APIKey. The compiler would hand the key over, and making parameters explicit doesn’t help, because an agent writes the calling code and will pass whatever the library asks for. A required interface that says “a JSON parser that only uses Console” makes the build fail. Writing these by hand was always too tedious, but agents can generate them, and they’re the first thing a human should review: the program’s capability footprint.

Slide: A supply-chain attack, excess authority and exfiltrated capability

Refinement types and model-written proofs. Types like “a double ≥ 0” or “a sorted vector” turn subtyping into logical implication. Today those checks go to runtime tests or an SMT solver. Since models have become very good at proof search, Odersky suggests letting them write the proofs, checking them offline, and treating an unproven implication like a red test rather than a compile error. He’s careful about the claims that all software will soon be formally verified: the hard part is writing the spec (“what’s the spec of Microsoft Word?”), but plenty of code can be specified, and more of it should be.

Slide: Refinement types workflow

Key takeaways

  1. Odersky treats agents as flaky compilers. Their output has to be constrained by something outside the model, because prompting and waiting for better models don’t give you guarantees.
  2. Sandboxes, allow lists and confirmation prompts all miss multi-step leaks where each step looks harmless. Information-flow tracking does catch them.
  3. Capability tracking in Scala 3 lets the compiler reject agent code that would leak classified data, before it runs, while agents stay about as effective as with ordinary tool calling.
  4. The dual LLM pattern can be enforced with types: overload resolution sends classified data to a local model and everything else to the cloud.
  5. Spec strings keep prompts in the source tree, so a reviewer reads intent and signatures instead of every generated line.
  6. Consumer-side required interfaces would make a dependency’s capability footprint explicit and stop supply-chain attacks that rely on agents passing along whatever a library asks for.
  7. Models that are good at proof search make refinement types practical, provided failed proofs are treated like failing tests rather than build breaks.

Source