Nate Foster on The Network as a Program

Nate Foster — professor of computer science at Cornell, co-creator of the network programming languages P4 and NetKAT, and visiting researcher at Jane Street — joins Ron Minsky to argue that a computer network is just another program: one that can be specified, composed, tested, and formally verified, instead of being configured router by router by hand.

Key ideas

1. Software-defined networking treats the entire network as a program, not a collection of manually configured boxes. Before SDN (software-defined networking — the idea, now roughly fifteen years old, that network behaviour should be expressed in software rather than vendor-specific device configurations), changing how a network forwarded traffic meant hiring a team of engineers to log into individual switches and edit low-level configuration files. SDN replaces that with a higher-level description — a program — from which the configurations for every device can be generated automatically, making the network as malleable as an ordinary software application.
2. NetKAT grounds network packet-forwarding in a clean mathematical theory, giving verification almost for free. NetKAT (Network Kleene Algebra with Tests) is a domain-specific language Foster and colleagues designed for describing how packets move through a network’s forwarding layer — the part of the network that decides, packet by packet, which port to send traffic out of. The language was discovered to align precisely with Kleene algebra with tests, a decades-old mathematical framework. That alignment means the tools of formal language theory — automated theorem provers, model checkers, SAT solvers — can be applied directly to check network properties such as ‘these two hosts can always reach each other’ or ‘these two tenants are completely isolated’.
3. P4 lets programmers specify the behaviour of individual switches, not just routing tables. Where OpenFlow (the earlier SDN standard) assumed a single lookup table inside every switch, P4 is a language that exposes the full programmable pipeline of a modern router or network-interface card. Foster spent a sabbatical at Barefoot Networks, the programmable-switch startup later acquired by Intel, to understand hardware deeply enough to design P4’s abstractions — a deliberate move to close the gap between PL theory and industrial networking practice.
4. Butane compiles a high-level network policy into BGP configurations for every router in Jane Street’s wide-area network. BGP (Border Gateway Protocol) is the routing protocol that underpins both the public internet and many large private networks: each router exchanges ‘path advertisements’ with its neighbours and makes local decisions about which routes to prefer. Jane Street’s network previously required engineers to edit BGP configs on individual routers; Butane is a system Foster helped design that lets engineers instead express intent at a higher level — latency requirements, traffic classifications, site-to-site preferences — which the compiler then translates into per-router BGP fragments. Changes are code-reviewed and tested against a formal model before they touch the network.
5. Formal methods in networking unlock exploration, not just bug prevention. The conventional picture of formal verification is a safety net: you specify what you want and a tool checks whether the current system satisfies it. Butane’s semantics enables a more expansive use — ‘what-if’ analysis of proposed changes before they are deployed, capacity-planning against historical traffic patterns, and (still in research) automated synthesis of the configuration change that would resolve a given congestion or latency problem. The model acts as an always-available simulation of the live network, enabling engineers to take bigger, faster steps with confidence.

Content

From physics to programming languages — and a career-defining detour

Foster’s route into computer science was indirect. He switched from physics during college after discovering that CS gave him the same satisfaction as physics’ unifying elegance, while adding creative latitude: abstractions like the lambda calculus or functional programming are human inventions, yet they run on physical machines. He completed a PhD at the University of Pennsylvania under Benjamin Pierce, where his primary work was on lenses — a family of abstractions for synchronising data between two representations. (A lens in this sense is a single piece of code from which two inverse functions — ‘get’ and ‘put’ — can be derived; the idea later became influential in Haskell’s ecosystem, though in a generalised form that loosened some of the original mathematical constraints.) After graduating, he joined Cornell’s faculty, where he spent fifteen years — and felt he had exhausted his best lens ideas.

The real turn came when he took a postdoc at Princeton with Jennifer Rexford and David Walker, entering networking with no prior background. The gamble paid off. He found the networking community unusually permeable between academia and industry: hyperscalers, switch vendors, and university researchers all identify as members of the same research community, which compresses the time between an idea and its adoption in production. He contrasts this with his home field of programming languages, where the same ideas (garbage collection, type systems) sometimes took forty years to reach mainstream use.

Software-defined networking: the idea and its reception

Starting around 2010, the networking world underwent a shift that Foster describes as inevitable from a programming-languages standpoint. Large cloud companies were building data centres at scales where the old model — configure each switch separately, coordinate through standards bodies to introduce any new behaviour — was too slow and too fragile. The SDN movement proposed instead that network behaviour should emerge from a program: a single description, checked into a repository, from which all device configurations are compiled.

Foster’s own slogan — ‘the network should just be thought of as another program’ — sounds trivial but cuts against decades of networking tradition, in which innovation was driven by hardware vendors shipping new router features and by standards bodies ratifying new protocols. The SDN vision says: just as a software team does not need Intel’s permission to deploy a new algorithm, network operators should be able to express new forwarding behaviours and have them realised in software on programmable hardware.

That vision has largely prevailed, though not in every detail its originators expected. Logically centralised control — a single controller deciding routing for an entire network — has not become standard; distributed protocols such as BGP still run the data plane. And fully programmable switch pipelines, while technically achievable, have not displaced commodity hardware for most workloads. Foster attributes this partly to economics and partly to the internet’s inherent conservatism: the same global scale that makes the internet resilient also makes it nearly impossible to change (‘ossification’, in the community’s word).

NetKAT: aligning networking with mathematical structure

The most technically foundational part of Foster’s work is NetKAT. The language was designed to describe the forwarding behaviour of a network: not how routing decisions are made (that is the ‘control plane’) but how packets are processed hop by hop — parsed, matched against tables, rewritten, and forwarded out of a port (the ‘data plane’). After several years of building domain-specific languages for this purpose, Foster’s group realised that their constructions matched a pre-existing algebraic system called Kleene algebra with tests, or KAT — a framework that Dexter Kozen at Cornell had developed over decades as a clean mathematical model of imperative programs.

The alignment meant several things at once. It gave NetKAT a principled semantics rather than an ad-hoc design; it connected the language to a rich body of theory about finite automata and regular languages (the same theory underpinning regular expressions); and it provided off-the-shelf constructions for building compilers and verification tools. Foster has since extended NetKAT with probabilities — necessary for networks where traffic volumes and failure patterns are uncertain and load-balancing is randomised — using the KAT structure to guide the extension and avoid incoherence.

Verification using NetKAT or related tools (SAT solvers, model checkers) on snapshots of a network’s forwarding state is now, in Foster’s assessment, fully reduced to practice at large cloud operators. An engineer proposing a change that would violate an isolation or reachability property receives an alert before the change is pushed. The remaining hard problem is that networks are distributed systems, and a snapshot captures only one moment of a system that is continuously changing — failures, control-plane updates, and unexpected interactions are not captured by a static model.

P4 and the Barefoot sabbatical: learning hardware from the inside

OpenFlow, the first SDN standard, modelled a switch as a single lookup table: you specify entries, the switch matches packets against them, and the matched entries determine what to do. This was a useful simplification for a first-generation language, but it obscured the real structure of high-speed switches, which have multi-stage programmable pipelines with specialised units for parsing, matching, and rewriting. Compiling arbitrary OpenFlow rules onto that pipeline proved unexpectedly difficult.

P4 took a different approach: expose the pipeline structure directly. A P4 program specifies how the parser works, what tables exist at each stage, and how control flows between them. The language is deliberately constrained — no dynamic memory allocation, no recursion — because every packet must traverse the pipeline at line rate, which may be hundreds of millions of packets per second. Expressiveness is sacrificed for determinism and speed.

Foster spent a sabbatical at Barefoot Networks — the company that built one of the first fully programmable switch chips — to understand the hardware on its own terms. He describes this as closing an ‘imposter syndrome’ gap: he had been designing network programming languages without fully understanding what the underlying machines could do. Barefoot’s team of veterans from Texas Instruments and elsewhere showed him the complexity of chip design, physical layout, and manufacturing. The technical idea that emerged from this period, developed with Barefoot colleague Changhoon Kim, was that a programmable switch chip is essentially a specialised processor — one with very high throughput and deterministic timing, suited to functions beyond packet forwarding: in-network computing, network telemetry, load-balancing coordination.

BGP, Butane, and bringing SDN ideas to Jane Street

BGP — the Border Gateway Protocol — was designed as the routing protocol for the internet. Each autonomous system (the internet’s term for an independently administered network, such as a company or a university) announces to its neighbours which IP address ranges it can reach and via which paths; neighbours propagate those announcements further; and each router makes local decisions about which path to prefer. BGP’s richness comes from the ‘attributes’ that can be attached to path announcements: cost, traffic-engineering tags, community markers, and other metadata that lets each router express fine-grained preferences.

The same protocol is widely used inside large organisations, not just between them, because it is expressive, well-supported by vendors, and already understood by network engineers everywhere. Jane Street’s wide-area network — connecting trading sites globally — had grown to the point where managing individual BGP router configurations by hand was reaching its limits. Engineers who wanted to move traffic onto a faster path had to edit configurations on multiple routers, with no systematic check that the combined result would produce the intended behaviour.

Butane, the system Foster helped design at Jane Street, inserts a compile-and-verify layer above the router configurations. Engineers write Butane policies — expressing latency preferences for different classes of traffic, structural expectations about how sites should relate, and traffic-classification rules — and the compiler generates the corresponding BGP configuration fragments for every router in the network. The change is then validated against a formal model of BGP semantics (informed by prior academic work, including a formalisation in the Rocq proof assistant by Zachary Tatlock’s group at the University of Washington) and can be visualised before it is pushed. Foster notes that the abstraction was kept deliberately simple — closer to a thin façade over BGP than to a radically different policy language — because the team wanted engineers to be able to ‘peel back’ the abstraction and understand exactly how a policy choice would map onto BGP config when they needed to.

The tooling for visualisation and testing has turned out to be at least as valuable as the compiler itself. Engineers can see the predicted change in latency between sites before committing a change, explore ‘what if a link fails’ scenarios, and, most recently, use the model for capacity planning: given historical traffic patterns and the current Butane policies, which new links would most improve throughput or reduce latency?

Formal methods as exploration, not just safety

A recurring theme in the conversation is the reframing of formal verification. In its conventional presentation, formal verification is defensive: you write a specification, build a model, and check that the system satisfies it. The deeper value, Foster argues, is that having a trustworthy model enables a different relationship with change. Instead of being conservative about network modifications — the traditional network engineering culture, where saying ‘no’ is part of the job — engineers can take larger steps because the model can evaluate those steps quickly and cheaply. Automated synthesis (proposing a configuration change that resolves a given problem while satisfying all existing constraints) is the next step beyond interactive exploration, and is still active research in Foster’s Cornell group.

The broader research direction connects to routing algebras, an algebraic framework for understanding BGP-like protocols developed by Tim Griffin and others, which models routing as an algebra of path preferences and selection rules. Two algebras can be ‘glued’ into a third — combining, for example, a latency-optimising policy and a bandwidth-optimising policy into a single protocol. The framework also clarifies when a distributed routing system will converge to a stable state (the Gao–Rexford conditions are a special case of this theory). Foster’s group is now exploring whether routing algebras could serve as the intermediate representation for a richer Butane compiler that generates distributed BGP implementations from truly high-level intent specifications.

On research culture and productive failure

Foster closes with a defence of exploratory research and honest retrospection. He helped organise a conference called Nines for the networking community, explicitly designed to surface new ideas rather than proven results. One invited talk — Scott Shenker on ‘What I got wrong about QoS’ (Quality of Service: the suite of protocols from the 1990s intended to give guaranteed bandwidth and delay to specific traffic flows, which mostly failed in deployment) — exemplifies the culture Foster wants: senior researchers publicly examining why ideas they championed did not prevail. Foster applies the same honesty to his own career: fully programmable switch pipelines, centralised SDN controllers, and certain aspects of P4 have not played out as the community anticipated. He regards this as healthy — communities that enforce orthodoxy calcify, while those that welcome and analyse failure remain capable of genuine innovation.

Related

• Nate Foster — speaker
• Ron Minsky — host
• Stephen Dolan on Memory Management, Garbage Collection, and OCaml — fellow Signals and Threads episode; adjacent deep-dive into programming-language theory applied to systems
• Doug Patti on State Machine Replication, and Why You Should Care — adjacent Signals and Threads episode on distributed-systems correctness
• Chris Perl on Clock Synchronization — adjacent Signals and Threads episode on network-level infrastructure problems at Jane Street
• The Future of Software Engineering — theme; the conversation illustrates how formal methods and software practices are transforming infrastructure engineering