把整個網路當成一支程式來寫：Nate Foster 在 Signals and Threads 聊網路的下一步

TL;DR

• 過去管網路是一台一台 switch 慢慢設定，靠資深網路工程師手動微調；Software Defined Networking 的核心觀念是把整個網路當成一支「程式」來寫，能用軟體的速度迭代、用軟體的工具驗證。
• 這套想法十五年前還很前衛，現在已經是業界常態，連學者投論文都被退稿說「你寫的就是現在大家做事的方法」。
• 把網路寫成程式最大的好處不只是抽象漂亮，而是能套用軟體那套版本控制、code review、測試、形式化驗證的文化，改設定前先算清楚會不會搞爆其他地方。
• Jane Street 內部用一套叫 Butane 的系統，把高階意圖編譯成一台台 router 的 BGP 設定，工程師最愛的居然是那個能預測「改完延遲會怎麼變」的視覺化工具。
• Multicast（群播）在雲端世界幾乎被放棄，但在交易這種特殊場景反而活得很好，這就是換個約束條件就會長出完全不同解法的例子。

先認識一下這集的來賓

這集在 2026 年 6 月 1 日上架的 Signals and Threads，是 Jane Street 自家做的技術 Podcast，主持人 Ron Minsky 是公司待了二十多年的老臣，當年主導 Jane Street 全面轉用 OCaml 這個函數式程式語言。節目一向專挑技術棧裡最硬的層面來聊，從時脈同步、可重組硬體到編譯器最佳化都有。

這集的來賓是 Nate Foster。他同時是 EPFL（瑞士洛桑聯邦理工學院）的教授，研究團隊今年一月才從 Cornell 搬過去，另外每週還抽一天當 Jane Street 的訪問研究員，跟網路團隊一起做事。Foster 的研究就卡在「程式語言」和「網路」的交界，他是網路程式語言 Frenetic、NetKAT 的主要作者，這些工作拿過 ICFP 最具影響力論文獎。簡單說，他是把寫程式那套理論搬進網路世界的開山人物之一。

一個失敗的物理系學生，怎麼栽進這行

Foster 自己講，他大學一開始念物理，越念越沒勁，倒是旁邊修的 CS 課讓他整個人投入進去。他喜歡的點很妙：物理是在研究大自然，而電腦科學研究的是人類自己造出來的東西，像 lambda calculus、函數式程式設計，這種拿來當運算基礎的抽象概念根本是人憑空設計出來的，居然還真的能在電腦上跑。

他講了一個我覺得超有意思的冷知識。垃圾回收（garbage collection，自動幫你管理記憶體、不用手動釋放）這個大概是程式語言史上對生產力幫助最大的發明，從發明到真正被主流語言廣泛使用，中間隔了大概四十年。四十年。一個這麼好的東西要等這麼久才被大家用上，這件事本身就很值得玩味。語言設計這條路有多慢，之前在Anders Hejlsberg 四十年寫四個程式語言的設計筆記裡也聊過類似的時間尺度。

把網路當程式，到底在解什麼問題

先講一個概念。以前管一個大網路是這樣的：你先想好機器要怎麼擺、怎麼接線，買一堆 switch 跟 router 接起來，然後請一票網路工程師很小心地一台一台設定，求它不要爆、求你要的資料流得對。

問題出在十五年前左右。Google、Amazon 這些公司的網路越長越大，動輒幾十萬台機器，各種協定、控制演算法堆在一起複雜到管不動，他們又想要能用軟體的速度自己改網路行為，不想每次都去拜託硬體廠商或等標準組織開會。於是 Software Defined Networking 就冒出來了，核心一句話：網路應該被當成另一支程式。

這句話聽起來廢，但對網路圈是思維大地震。Foster 打了個我很喜歡的比方：我們要在硬體上跑新演算法，不會先去跟 Intel 或 NVIDIA 申請許可，直接寫支程式就好；那網路為什麼不能有同樣的自由？

不過要講清楚，網路這支「程式」跟你在伺服器上跑的程式不一樣。網路速度太快、規模太大，你不可能對每個封包、每一跳都去動態配置記憶體，那會瘋掉。所以它是個有特殊約束的領域。但神奇的是，Foster 他們發現這套東西居然能對上一個叫 KAT（帶測試的 Kleene 代數）的數學框架，那是 Cornell 的 Dexter Kozen 搞了幾十年的理論。從一個看起來全是怪規則的領域，硬是抽出一個長得像有限自動機、狀態機的東西，這就是程式語言理論的「一個小撇步」:把亂糟糟的人類活動，接到一個夠簡單的數學模型上，後面加的新功能往往就自動長得很順、彼此組合得很好。

真正的價值，是把軟體那套文化搬進來

Ron 在這裡補了一個我覺得比抽象漂亮更實在的觀點。SDN 的好處不只是語意變乾淨，而是它讓你能把軟體工程那一整套文化搬進網路：版本控制、code review、測試、把設定檔丟進 repository 讓人審。

舊世界裡，網路工程師就是直接登進 router，然後 YOLO 改一發。改錯了，整個網路就出事。你常聽到大公司因為一個 config 改動造成大當機，問題幾乎都出在這:某個設定改下去，產生了你沒預期到的行為。

把網路寫成程式之後，你就有一個集中的地方可以驗證。改路由之前先問：這會不會把別處的連線弄斷？這就接到了形式化驗證（formal methods，用數學方法證明系統行為符合規格）。形式化驗證怎麼從冷門領域變成基礎建設防火牆，之前在Byron Cook 拆解 Formal Methods那篇講得更細。

但 Foster 也很誠實：這領域遠遠沒做完。網路本質是分散式系統，有你沒想到的故障、沒納進模型的互動，人為失誤造成的當機到今天還是天天在發生。

Butane：Jane Street 怎麼把這套真的跑起來

Foster 在 Jane Street 做的東西叫 Butane。Jane Street 的全球網路越來越大，但以前還停在「一台台改 BGP 設定」的石器時代。

BGP 是當年為整個網際網路設計的路由協定。網路上幾萬個自治系統（autonomous system，每個組織就是一個），各自決定怎麼把流量導到別人那。BGP 的運作方式是每個節點告訴鄰居「要找 Jane Street 來我這、我一跳就到」，還能在這條廣告上掛各種屬性，像成本、標籤。每個 router 收到一堆通往同個目的地的路徑，自己挑一條它覺得最好的。它是個亂糟糟的分散式系統，但因為背後有經濟關係撐著（ISP 跟客戶的層級結構），它收斂得意外地穩。

Butane 做的事，就是讓你在一個集中的高階規格裡寫下你要什麼,比如「這類流量一定要走最快的路、那類流量能到就好，繞地球一圈我也認」，然後編譯器幫你產出每一台 router 的 BGP 設定。改網路的時候，你改一點 Butane config，編譯、驗證、推上去，不用再手動戳好幾台 router。

Foster 講了一個讓他意外的點。他本來以為網路工程師會嫌這套東西，結果大家最愛的不是抽象本身，而是那個視覺化跟測試的工具。你改一個設定，UI 直接算給你看各站點之間的延遲會怎麼變。再往下做，還能玩「如果斷了 N 條線會怎樣」「我想讓這個熱點消失，給我一組改動建議」這種 what-if，背後就會用到程式合成、solver 那類技術。形式化方法在這裡的價值不只是抓 bug，而是讓你敢踏出更大步、甚至自動探索那些步。最近他們連買未來要鋪哪條線的容量規劃都拿這套模型來算了。

Foster 還坦白，Butane 的 policy 抽象其實做得相當保守，簡單到能直接對應到 BGP 設定，沒玩什麼花的。他說老實話有點小失望，本來想搞個更狂的東西。但回頭看，挑簡單、能在需要時掀開抽象看底層的設計，是對的選擇。這跟 OCaml 的哲學很像:既是高階語言，編譯過程又夠直白,你看程式碼大概就猜得到它會怎麼跑。

失敗的研究也很健康，還有 Multicast 這個反例

這集我最喜歡的一段，是兩人聊「做不成的研究」。Foster 講了好幾個他做過、最後沒變成世界主流的題目，網路內運算（in-network computing）到今天都還很有爭議。但他的態度是:大學研究就應該去試這些狂的東西，不是說你解不出來，而是它最後沒成為世界運作的方式，這完全沒關係。一個社群如果太保守、什麼都要照正統做法，那才是停滯的開始。網際網路會「僵化」到改不動，某種程度就是這樣來的。

Multicast（群播，把同一份資料一次發給很多人）就是個漂亮的例子。Foster 跟 Ron 講，當年大家以為 multicast 會是傳影片給所有人的方法，結果失敗了，雲端世界現在幾乎沒有真正的 multicast。但在交易這個場景反而活得很好,交易所就是用 multicast 把行情公平、有效率地發給所有人。為什麼外面失敗、這裡成功？因為要群播的頻道數量在交易場景少很多，當年壓垮 multicast 的控制平面成本問題，在這裡根本不成立。

這就是 Foster 一直在講的事:你把一個問題的某個假設換掉、加個新約束，往往就會逼出一個完全不同的解法。財務網路在乎的延遲尺度、multicast 的需求，跟 hyperscaler 不一樣，所以才有獨特的問題值得做。我自己讀到這段最大的收穫是，別太快用「業界主流都這樣做」去否定一個老想法,換個場景，被淘汰的東西可能正好是你要的答案。

整集聽下來，Foster 給我的感覺就是一個能在學術的狂想跟產業的落地之間自在切換的人。他每週只進 Jane Street 一天，謙虛地說自己是團隊裡的小角色，禮拜四傳送回來的時候，神奇的事都已經發生了。但正是這種一腳在理論、一腳在實作的姿態，讓「把網路當程式」這件聽起來很廢的話，慢慢變成真的能跑的系統。

這類橫跨學術跟產業的技術觀察我會持續寫，訂閱 wilsonhuang.xyz 就不會錯過。

Sources:

• Home - Nate Foster
• Appointment of EPFL professors - EPFL
• Signals and Threads Podcast