▶ YouTube Summaries

• YT :: https://www.youtube.com/watch?v=jlJyuJhDnlc
• Original title :: Martin Odersky – Keynote: The End of Programming? #ScalaDays

Martin Odersky opens Scala Days 2026 by asking whether coding agents mean the end of human programming. Agents now write and review most code, so programs become black boxes. Giving up the ability to understand software means handing the keys to agents, your own or an attacker's. LLMs are "flaky compilers" with no guarantees, so correctness has to be enforced from outside the model. His group's answer for agents is TACIT: agents write capture-checked Scala 3, and the compiler, not the model, rejects unsafe code before it runs. For large systems he floats three tentative ideas: spec strings that keep the prompt in the source, required interfaces that limit what a program may take from its dependencies, and refinement types whose proofs are written by models.

The problem

• Industry claims: software engineering automatable "in 12 months", 75% of Google code written by agents, companies with "no humans involved".
• Review is going away too. Agents review agents, and humans don't want to read avalanches of generated code.
• The usual workflow is prompt, then AI program, then tickets fed back to the agent. The program stays a black box, and in that world languages only matter for tokens and speed, not readability, modularity or safety.
• Abandoning software understanding is a "singularity" through human dereliction of duty, not through an intelligence explosion.
• Raising abstraction the way assembly gave way to C doesn't quite work: agents are non-deterministic, so control must be external, not "please don't make mistakes".

Agents are already there

• Tool-calling agents generate small code snippets that run immediately and that nobody reads. Result: leaked credentials, deleted mail, agent swarms breaking into Hugging Face and Australian Medicare.
• Two challenges: contain agents, and build software that resists agentic attacks.
• Current defenses fall short: allow/block lists are too coarse, user confirmations cause click fatigue, sandboxes give all-or-nothing permissions.
• The real need is information-flow tracking, because each step can look fine on its own while the whole chain leaks a secret.
• The lethal trifecta: private data, external communication and untrusted content. Removing any one of the three is impractical.

TACIT: tracked agent capabilities in types

• Key idea: don't make the model trustworthy, make the medium safe. Agents express intent in Scala 3 with capture checking; the type system tracks what code may do and the compiler enforces it.
• Analogy: a secret diary and builders. Lock the diary and hold back the key, the capability. To let an agent work with the secret without leaking it, use the dual-LLM ("Severance") model: one model faces the world, the other sees private data, and they can't talk to each other.
• Capabilities in types: String and Int -> Int are pure, File^{io} and Int ->{io} Int hold IO, File^ and =Int > Int may do anything. The single arrow now means a pure function; the double arrow keeps its old meaning.
• Classified[T]: reveal needs a capability the agent never gets, map accepts only a pure function (no printing, network or mutable state), aggregate combines classified values. Timing side channels are not covered yet. The same approach generalizes to multiple security levels and untrusted input (indirect prompt injection).
• chat(prompt, String) goes to the cloud model; chat(prompt, Classified[String]) goes to a local trusted model and returns Classified.
• Architecture: LLM writes Scala snippets, an MCP server compiles them with capture checking and runs them in a REPL against a capability-aware library.
• The paper Securing Agents with Tracked Capabilities won best paper at the first ACM conference on AI and agentic systems (May 2026). Open source on GitHub.
• Safe mode (language.experimental.safe) turns off unchecked casts, caps.unsafe, reflection and untrusted globals for agent code. Library classes marked @assumeSafe must be audited, similar to Rust unsafe.
• Evaluated on AgentDojo, SWE-bench and τ²-bench: safe under adversarial conditions and no less capable than ordinary tool calling. Example rejections from real runs: println inside Classified.map, and a filesystem capability escaping its scope.

Beyond agents: large systems

• Shared with agents: the goal is trust without reviewing every line, and strong types bound behavior.
• Different: agent code lives seconds to hours and is about ten lines, fully opaque; programs live for decades, run to millions of lines and can be partly reviewed.
• Kent Beck: agent work feels like being an air-traffic controller, interrupt-driven, with flow lost.
• "Everything changes but programming languages stay the same" is unlikely; how they will change is still open.

Three tentative ideas

• Spec strings :: the prompt stays in the source. The AI's job is to keep code in sync with human-written specs, and a change request edits the spec. The spec doubles as documentation, and types bound what the generated code can do.
• Required interfaces :: the consumer declares what it needs from a dependency, e.g. required object JsonParser uses Console { def parse ... }. This defends against supply-chain attacks such as a new library version asking for Network plus an implicit API key, which an agent would hand over without a second thought. Writing these used to be too tedious, but agents can generate them, and they are the first thing a human should review: the program's capability footprint.
• Refinement types and proofs :: types like Double with x > 0=, a sorted vector, or an index within bounds. Subtyping becomes logical implication, checked today at runtime or with an SMT solver; next, models write the proofs and the proofs are stored with the code. Checking runs offline, and a failed proof works like a red test rather than a fatal error. Caveat: most software, like Microsoft Word, has no formal spec.

Takeaways

• Meaningful oversight is still required, but not line-by-line review.
• Languages should keep code from turning into a ball of mud, which agents speed up, so essential behavior fits in concise signatures that allow small, high-confidence reviews.
• Building blocks: types, capabilities, modules, formal and informal specs, formal verification. Expect years of experimentation.