Trustworthy Human-AI Collaboration in a Live Type-Theoretic Computational Commons

实时类型论计算公地中值得信赖的人机协作 Cyrus Omar 剖析了现代软件工程中快速反馈循环失效的问题，指出语法错误和缓慢的编译周期如何让程序员与 AI 智能体同时陷入盲区。通过展示 Hazel，他说明了错误恢复解析器、一等类型孔洞（typed holes）和实时动态探测器如何让程序即使在不完整的情况下也能保持持续可执行与可分析。他将这些概念拓展至智能体工作流，提出使用结构化抽象语法树（AST）框架取代原始 Bash 接口，以减少上下文开销并防止幻觉循环。为安全协调大规模智能体集群，演讲概述了一种将图 CRDT（Grove）和内容寻址代码（Unison）与不可伪造的对象权能相结合的架构，以严格执行最小权限原则。最后，Omar 展示了作为全球实时相互依赖模块网络的计算公地，该公地有能力为行星气候模型等大规模科学模拟提供支持。 Cyrus Omar 展示了一个实时的类型论计算公地，它结合了 Hazel 的类型孔洞语义、Grove 的图 CRDT 以及 Unison 风格的内容寻址存储，以支持人类与 AI 智能体的并发开发。 (0:00) Hazel 通过将不完整的语法和缺失的定义视为一等类型孔洞来填补开发者工具的不足，使求值、实时探测检查和增量类型检查能够不间断地运行。 (3:29) 为降低自主智能体因使用宽松执行标记（如 Claude Code 的危险跳过权限）而带来的安全风险，该架构采用了不可伪造的对象权能令牌和信息流控制。 (44:36) 该协作模型正被应用于剑桥大学的“为地球编程”（Programming for the Planet）计划，旨在将复杂的气候子模型连接成一个持续更新的实时可执行网络。 (47:02)

Cyrus Omar argues that traditional software development is crippled by delayed feedback loops, broken toolchains, and file-based versioning, requiring a shift toward an incremental, live, type-theoretic computational commons suitable for both human developers and autonomous AI agent swarms. Resolving Developer Feedback Gaps with Hazel (3:29) Traditional programming environments force developers to write code without sensory feedback until full compilation cycles complete. Any intermediate syntax or static type error breaks editor services like autocomplete, halts execution, and forces programmers to parse dense textual logs. To eliminate this friction, Omar demonstrates Hazel, an environment co-designed around typed holes and live error recovery. Syntactically incomplete expressions are represented as explicit hexagonal holes, allowing the type checker and evaluator to continue running rather than crashing. Using live probes, developers can inspect runtime data, observe intermediate recursive frames, and catch logic bugs—such as duplicated pivot elements in a quicksort implementation—immediately as tokens are entered. Incremental Semantics for AI Agent Swarms (31:48) Omar observes that autonomous AI agents face the same feedback bottlenecks as human programmers, exacerbated by their stateless nature and the need to repeatedly re-establish context. Compiling and running whole programs across agent tasks consumes excessive time and burns tokens parsing logs. In response, Hazel uses expression-level incrementality and shortcut memoization to cache sub-expression evaluation results across abstract syntax tree edits, bypassing whole-program recomputation. Rather than restricting models to unstructured terminal shells, Hazel exposes a structured action language where agents perform surgical AST edits, leverage semantic symbol navigation, and inspect inline probe feedback directly within their observation context. Tree CRDTs and Object Capabilities (41:32) Uncoordinated agent swarms collaborating over standard text-based Git repositories easily fall into destructive conflict loops, occasionally wasting tens of thousands of dollars in tokens on minor stylistic merges. To coordinate concurrent edits cleanly, Omar's team developed Grove, an abstract syntax tree collaborative editor based on graph CRDTs that treats code relocation as a first-class commutative primitive to eliminate silent duplications. To manage security risks when agents operate autonomously, the system enforces object capabilities rather than blanket shell access. By attenuating unforgeable capability tokens—such as restricting an agent to append-only logging—the environment guarantees least-privilege security and enforces strict information flow boundaries. The Computational Commons and Content Addressing (47:02) Omar envisions organizing software into a global computational commons modeled like a resilient, live-executing encyclopedia, where localized errors are isolated by typed holes rather than crashing downstream consumers. Interactive documents embed rich graphical literals, such as data tables and sliders, and connect to massive remote datasets via a Foreign Data Interface that pushes functional computations down to SQL and Spark backends. To resolve the tension between continuous live updates and production stability, the architecture integrates Unison's content-addressed code model. Because functions are referenced by immutable cryptographic hashes of their syntax trees rather than mutable text names, agents can author updates in parallel without breaking existing dependencies. While modern AI eliminates historical barriers to bootstrapping new languages by porting libraries overnight, scaling continuous liveness to collaborative environments introduces open challenges. Managing massive recursion traces on screen, standardizing structured change tours for human review, and balancing real-time reactive execution against deliberate release processes remain active areas of research.

Cyrus Omar在Jane Street的演讲中指出，传统软件开发工具链因语法与类型错误切断动态反馈，阻碍了人机交互；他提出利用类型孔洞、细粒度增量求值、内容寻址与对象能力，构建一个面向人类开发者与AI代理群的实时类型论计算公域。 开发工具反馈缺口与Hazel活编程环境 (3:29) Omar以钢琴演奏等物理工具的即时感官反馈为例，对比了传统软件工程中开发者在黑暗中编写代码、等待编译报错的断裂循环。常规工具链存在“缺口问题”（the gap problem）：一个局部的语法或类型错误就会导致跳转定义、自动补全等编辑器服务彻底崩溃，并完全阻断动态运行时求值。开发者只能在经历漫长重新编译后面对难以高效解析的庞大文本日志。 为弥补该缺口，Omar展示了其实验性函数式编程语言与环境Hazel。Hazel引入由David Moon设计的容错解析器，当代码未写完（例如let表达式中in之后缺失主体）时，系统不会报致命语法错误，而是自动合成显式的六边形“类型孔洞”（typed hole）。孔洞在类型系统中属于一等公民，允许未完成的代码保持静态可分析与可执行状态。通过在调用处附加实时探针（probe），开发者与测试用例可以在未完全实现辅助函数的情况下，直接观察部分求值的调用栈并切换不同测试样本。 实时执行语义、渐进类型与图形化表达 (9:24) 在活编程演示中，Omar在编写快速排序的划分函数时故意引入逻辑错误（将pivot而非head填入子列表，以及写反比较符）。由于代码本身类型正确，传统静态检查会保持沉默，而Hazel的探针直接呈现出全为3的列表以及倒序切分结果，使逻辑缺陷在编写当下即时暴露。针对无限循环与副作用，Hazel采用受限求值策略：当递归深度触及上限，系统将对应调用就地替换为类型孔洞以隔离故障，防止编辑器崩溃；同时语言核心保持纯函数式，通过类似Haskell的纯动作描述（如monadic IO）隔离副作用，避免每次击键都触发真实I/O或交易。 Hazel的渐进类型系统支持包含未知类型的表达式，并利用合一约束进行类型推断。在执行层面，环境引入了“Probarium”侧边栏用于检查递归层次、固定特定调用栈帧，并支持在探针与源码中直接内嵌表格、滑动条、二维触控盘和实时音频合成等图形化表示。针对大规模执行开销，架构规划了分级执行体系：小样本依托深度插桩的解释器进行实时调试，大规模数据输入则交由即时编译器（JIT）运行。 AI代理协作瓶颈与细粒度增量IDE (29:17) 随着软件开发转向AI代理主导，Omar指出多代理协同系统同样受到反馈延迟的制约。尽管前沿大语言模型鲜少犯初级语法错误，但在遇到类型不匹配时同样会丢失动态反馈。由于代理在启动时缺乏长期记忆（“金鱼记忆”），依赖全量重编译和冗长终端文本日志不仅产生巨大延迟，还会消耗天价Token。当未来晶圆级ASIC将推理吞吐提升至每秒1000个Token以上时，环境工具链的验证延迟将成为整个系统的核心瓶颈。 为应对该问题，Hazel将增量性推进至语法树表达式层级。其快捷备忘录（Shortcut Memoization）技术利用模式抽象备忘表跨代码修改保留中间求值状态，新测试的加入仅触发必要的子表达式计算，静态类型检查也无需重新跑完完整流水线。Hazel为此构建了专为AI代理设计的结构化动作语言，使代理能通过语法树替换精确操作代码，直接消费探针输出的执行上下文。针对人工代码审查积压问题，Omar与Hannah Potter开发了叙事化变更导览（narrativized change tour），通过带有完整性检查的架构叙事取代机械的字母序Git差异对比。 树形CRDT、内容寻址与对象能力安全 (41:32) 针对大规模代理群并发修改同一代码库引发的冲突循环（曾有案例因缺乏协调在LLM Token上空耗5万美元），Omar的研究组开发了基于树形CRDT的协作编辑系统Grove。与Git基于文本行的合并机制不同，Grove将抽象语法树操作设计为满足交换律的动作，并将代码移动（relocation）设为一等原语，从根本上杜绝了因多方重构导致的静默重复定义。 在版本控制上，团队吸收了Unison语言的内容寻址机制。代码定义不依赖易变的文本名称，而是由其语法树的加密哈希唯一标识。添加新实现仅生成新的哈希条目，历史引用保持不变，允许数千个代理在互不阻塞的前提下并行探索或重构，随后再进行统一合并。而在执行权限管控上，Omar强调必须抛弃宽泛的终端Shell访问与高危越权设置，转向对象能力（Object Capabilities）架构。通过类型系统签发不可伪造的轻量权标，并利用能力衰减（attenuation）实现最小权限控制（如仅允许向单一日志文件追加内容），从形式化层面防范代理的破坏性操作与数据越权流动。 行星级计算公域与现代化语言重构机遇 (47:02) Omar将其技术构想总结为“实时类型论计算公域”（Live Type-Theoretic Computational Commons）。该架构类似维基百科，但每个页面都相当于一个实时运行的类型化模块；局部的语法或类型错误被类型孔洞安全隔离，仅影响下游依赖。Omar计划在剑桥大学休假期间推进“Programming for the Planet”项目，通过外部数据接口（FDI）将下推谓词编译为Spark或SQL查询，将海洋水温、冰原动力学与生态模型链接为单一可执行网络。此外，Hazel正在构建Isabelle风格的高层不变量证明层，以便AI自动生成证明、人类工程师仅需专注审查规范。 面对计算范式变迁，Omar提出“因羡慕而转化”（translation by jealousy）的推广哲学。他强调，过去构建新语言需要数亿美元与漫长周期来克服网络效应和标准库匮乏，而今借助大语言模型（如让Claude通宵生成），新语言的标准库与现有笔记本可以低成本自动化迁移。这使得计算机科学界不再被迫屈就于历史技术债务，有能力自底向上重塑软件工程的基础抽象。 实时计算公域展现了消除传统构建、部署界限的潜力，但若缺乏对生产稳定性的严格把控，全天候实时响应亦可能引发系统性混乱。Omar主张将Unison不可变的内容寻址与显式迁移流程相结合，以在技术工具消除构建复杂度的同时，保留严谨的人工工程裁决。

## Background 该视频由金融与科技公司 Jane Street 于 2026 年 9 月 11 日在 YouTube 平台发布。视频记录了 Cyrus Omar 的前沿学术讲座，内容围绕其团队开发的 Hazel 实时编程环境展开，旨在构建一个融合 CRDT 结构化编辑、Unison 式内容寻址以及类型论对象能力沙箱的“实时类型论计算公域”（Live Type-Theoretic Computational Commons），以支持人类与大规模 AI 智能体蜂群的安全并发协作。 ## TL;DR Cyrus Omar 探讨了现代软件工程中因语法与类型错误导致的“裂隙问题”，并现场演示了基于类型孔洞（typed holes）、容错解析与实时探针的纯函数式编程环境 Hazel。随着研发范式转向高吞吐量的多智能体系统，传统 Bash 终端与纯文本 Git 协作面临严重反馈迟滞与并发冲突，团队为此提出了细粒度表达式增量计算、模式化记忆（Shortcut Memoization）及面向树结构的图 CRDT。为了解决智能体越权带来的安全隐患，他进一步提出了不可伪造的对象能力衰减架构与信息流控制，最终展望了一个具备容错韧性、可支撑气候科学等复杂跨学科建模的维基百科式活态计算网络。 ## Atmosphere & style 整场演讲洋溢着浓厚的高阶学术探索与极客幽默氛围，Cyrus 在黑板风格的投屏前一边从容敲击代码，一边与台下经验丰富的工业界工程师机智交锋。演示过程中诸如“哎呀，全是三”的即兴捉虫、失控的算法节奏节拍以及现场关于“危险地跳过权限”的调侃，频频引发全场会心大笑。随着话题从微观的 AST 编辑步步推演至行星级气候建模与类型论本体论，现场在充满学术锋芒的质疑与严密回应中，展现出一种打破陈旧软件基础设施、重塑人机共生未来的激进与乐观。 ## Bulletin - [03:29](https://www.youtube.com/watch?v=fB_lklm7xgU&t=209s) 传统开发工具因代码局部语法或类型错误而导致 IDE 服务和执行全面瘫痪的“裂隙问题”，可通过容错解析器生成的具名一等语言构造“类型孔洞（typed hole）”化解，使不完整代码仍能持续进行类型检查和符号化求值。 - [29:26](https://www.youtube.com/watch?v=fB_lklm7xgU&t=1766s) 面向千级 Token/秒的超高速 AI 智能体，工具链本身正在成为新瓶颈；基于结构化动作语言与内联求值探针的增量 IDE 能让智能体避免全量代码重写和盲盒调试，实现低成本的即时自我验证。 - [41:32](https://www.youtube.com/watch?v=fB_lklm7xgU&t=2492s) 针对大规模智能体蜂群并发编辑容易引发的冲突风暴，Hazel 团队提出了基于树结构的原生可交换图 CRDT（支持代码重定位为一等原语），并融合 Unison 风格的内容哈希寻址以实现无破坏性的多版本安全共存。 - [44:32](https://www.youtube.com/watch?v=fB_lklm7xgU&t=2672s) 在智能体沙箱安全方面，团队主张采用对象能力（Object Capabilities）架构实现权限衰减与信息流控制，彻底消除为图省事而滥用“跳过权限确认”带来的根级别安全隐患。 ## Key takeaways - [00:00](https://www.youtube.com/watch?v=fB_lklm7xgU&t=0s) 人机交互中最基础的反馈回路应满足及时性与低认知负荷，但当代软件工程普遍存在“必须全对才能获得反馈，稍有错误需等待数分钟且仅获延迟报错”的反直觉现状。 - [03:29](https://www.youtube.com/watch?v=fB_lklm7xgU&t=209s) 开发者工具链中的“裂隙问题”（The Gap Problem）源于轻微语法或类型错误对抽象语法树（AST）解析的破坏，进而导致静态服务全面断裂、重编译耗时冗长且输出退化为海量文本日志。 - [06:19](https://www.youtube.com/watch?v=fB_lklm7xgU&t=379s) Hazel 通过容错解析器将未完成代码转化为显式的六边形类型孔洞，并支持挂载动态实时探针（Probes），使开发者在函数尚未实现或存在逻辑缺陷时即可观察到真实运行环境中的输入参数。 - [12:31](https://www.youtube.com/watch?v=fB_lklm7xgU&t=751s) 在处理并发与连续编辑时，Hazel 采用符号化求值与类似 Haskell 的纯函数式 Monadic I/O 隔离机制，防止击键触发高频重算时随意引发不可逆的外部副作用（如误触发金融交易下单）。 - [16:56](https://www.youtube.com/watch?v=fB_lklm7xgU&t=1016s) 渐进类型（Gradual Typing）与未完全求解的类型约束合一算法为孔洞提供了坚实的理论语义，使系统不仅能容纳未知类型（?），还能实现精准的错误局部化与多采样调用栈下钻分析。 - [26:09](https://www.youtube.com/watch?v=fB_lklm7xgU&t=1569s) 借助图形化表示法（Graphical Notation），纯函数式的数据流可直接映射为可交互表格、旋钮表盘乃至算法音乐控制台，UI 交互修改亦可反向生成对应的函数式代码变更。 - [29:26](https://www.youtube.com/watch?v=fB_lklm7xgU&t=1766s) 随着 ASIC 晶圆级硬件驱动 AI 生成速度突破 1000 Token/秒，软件开发的瓶颈将从人类手打代码转移到“智能体-工具”反馈回路；缺乏跨会话记忆的智能体极易被庞大且昂贵的终端编译文本日志拖垮。 - [33:06](https://www.youtube.com/watch?v=fB_lklm7xgU&t=1986s) 细粒度增量计算将优化从编译单元细化到单个 AST 表达式级别，结合即将在 LA 2026 发表的“快捷记忆化”（Shortcut Memoization），可在函数逻辑修改后依然跨版本复用中间计算结果。 - [36:56](https://www.youtube.com/watch?v=fB_lklm7xgU&t=2216s) 为 AI 智能体打造原生的结构化动作语言而非包裹一层 Bash 终端，能赋予模型语义搜索、跨作用域反查和行级内联数据验证能力，大幅削减修改全量文本带来的 Token 开销。 - [39:47](https://www.youtube.com/watch?v=fB_lklm7xgU&t=2387s) 面对 AI 引发的 PR 审查堰塞湖，“叙事化变更导览系统”（Narrativized Change Tours）将零散的 Git 文本块重构为符合逻辑的故事线，并辅以详尽性静态检查器防止审查遗漏。 - [41:32](https://www.youtube.com/watch?v=fB_lklm7xgU&t=2492s) 为解决多智能体协作中“解决冲突之冲突”的资源死循环，基于树的图 CRDT 将代码移动（Relocation）升格为一等原语，并利用 Unison 的内容哈希寻址确保代码只增不减、多版本安全并行。 - [44:32](https://www.youtube.com/watch?v=fB_lklm7xgU&t=2672s) 通过引入对象能力模型（Object Capabilities）和形式化信息流控制，系统可将全量 File I/O 细粒度衰减为只追加日志等受限能力，在数学证明层面阻断智能体数据越权与泄露。 - [47:02](https://www.youtube.com/watch?v=fB_lklm7xgU&t=2822s) “动态计算公域”（Live Computational Commons）愿景将代码库构建为类似维基百科的互联执行网络，单个节点的语法或类型错误被约束在局部孔洞中，从而支撑跨学科的大型行星级动态仿真建模。 - [55:14](https://www.youtube.com/watch?v=fB_lklm7xgU&t=3314s) 面对海量行星级外部数据无法全载入内存的问题，外部数据接口（FDI）借鉴 Apache Spark 的算子下推理念，将 Hazel 纯函数式变换在运行时直接转化为底层 SQL 调用或分布式执行引擎操作。 - [01:01:12](https://www.youtube.com/watch?v=fB_lklm7xgU&t=3672s) 大语言模型的普及颠覆了传统语言生态构建的成本结构，以往耗费数亿美元编写标准库和工具链的门槛大幅瓦解，为计算机科学界彻底重塑底层语言基石打开了关键窗口。 - [01:03:12](https://www.youtube.com/watch?v=fB_lklm7xgU&t=3792s) 在“一切皆实时运行”的计算体系中，“部署”的概念不再是全量发布更新，而是依托 Unison 式不可变 AST 内容哈希保证确定性版本引用，兼顾高频数据流持续推演与核心生产环境的绝对稳定性。 ## Detailed walkthrough ### [00:00](https://www.youtube.com/watch?v=fB_lklm7xgU&t=0s) 反馈循环：从钢琴与画笔到编译器 在简街资本（Jane Street）的演讲开场中，Cyrus Omar 阐释了其学术研究的一大核心主题——**反馈循环（feedback loops）**。他回顾道，在涉足程序设计语言领域之前，他曾从事大脑反馈机制与反馈信息论（Feedback Information Theory）的相关研究；而在大约 15 年前，他的注意力转移到了人机交互中最基础的反馈回路上：人类作为工具的使用者，向工具输入信息并驱动其运转，工具则实时反馈输出。 ```mermaid flowchart LR accTitle: 人机交互反馈循环对比 accDescr: 对比传统实体工具（即时感官反馈）与现代编程编译器（高延迟、全或无报错反馈）的闭环链路差异。 subgraph Physical["实体物理工具（如钢琴、画笔）"] P_Human["演奏者 / 画家"] -->|"击键 / 落笔"| P_Tool["乐器 / 画纸"] P_Tool -->|"即时声波 / 笔触（毫秒级）"| P_Human end subgraph Modern["传统编程开发（编译器）"] C_Dev["程序员"] -->|"离线编码（长盲区）"| C_Code["代码文件"] C_Code -->|"触发编译"| C_Comp["编译器 / 运行时"] C_Comp -->|"延迟报错 / 堆栈追踪"| C_Dev end ``` 好的反馈应当具备两大关键特质：**及时性（timely）**与**低认知负荷（not too onerous to process）**。在计算机诞生之前的传统工具中，这种瞬时闭环极为自然——按下琴键的刹那声音入耳，落笔纸面的瞬间墨迹立现，人类感官能够在毫秒级别处理这些感知输入。Cyrus 随即抛出了一个荒谬的假设反问： > “Imagine you're learning to play piano, right? And you press a key and you don't hear the note. Instead, you have to keep pressing keys for a while to complete the song. And you'll hear the song if you played it completely correctly. But if you made one wrong move in that song, you won't hear it at all and it'll just give you an error. And also, you won't get that error for about 3 minutes afterwards.”（“想象一下你正在学钢琴：按下琴键却听不到任何声音。相反，你必须连续弹奏很长一段时间把整首曲子弹完；只有在完全弹对的情况下，你才能听到整首歌。但凡弹错了一个音，你不仅什么都听不到，它只会给你弹出一个错误——而且这个错误通知还要等上足足三分钟。”） 现场引发一阵笑声。Cyrus 指出，这种反直觉的极端设定恰恰是当代软件工程的残酷现状：开发者长时间在没有动态反馈的真空环境中敲入代码，扔给编译器后往往得到冷冰冰的拒绝，随后只能在盲打与碰壁中反复试错。虽然现代开发环境通过实时语法高亮提供了一定程度的静态辅助，但只要源码中存在任何一处语法错误或类型不匹配，所有动态执行信息便会瞬间瘫痪，连已完工代码段的状态也彻底不可见。 --- ### [03:29](https://www.youtube.com/watch?v=fB_lklm7xgU&t=209s) 开发者工具中的“裂隙问题” 针对开发工具链中反馈严重迟滞、处理成本高昂的现状，Cyrus 提出了一个专有名词——**裂隙问题（the gap problem）**。无论是轻微的语法错误还是局部类型不兼容，都会在集成开发环境（IDE）的服务链路中撕开一道鸿沟，导致代码跳转（Go to Definition）等核心功能直接失效。 ```mermaid flowchart TD accTitle: 开发者工具中的裂隙问题 accDescr: 展示语法或类型错误如何级联阻断静态 IDE 服务与动态执行管道，最终输出高认知负荷的纯文本日志。 E["源码编辑中的细微缺陷（语法 / 类型错误）"] --> G["裂隙问题（The Gap Problem）"] subgraph GapStatic["静态语言服务中断"] G --> S1["语法解析树断裂"] S1 --> S2["跳转定义、自动补全失效"] end subgraph GapDynamic["动态执行链路坍塌"] G --> D1["编译与重编译耗时冗长"] D1 --> D2["全量代码被拒，无法部分执行"] D2 --> D3["最终产物退化为庞杂的纯文本日志（需肉眼检索）"] end ``` 这一困境的核心痛点包括： - **静态服务链断裂**：一旦代码某处出现类型或解析故障，依赖符号分析的编辑器服务（如代码导航、重命名、引用查找）便无法获取完整 AST，从而整体罢工。 - **重编译与再执行停滞**：代码即使发生微小的局部改动，系统往往仍需漫长等待，无法快速实现局部增量求值。 - **信息承载形式低效**：终端往往丢出一大堆难以被感官直接消化的纯文本日志（large textual logs），迫使程序员化身为“人肉解析器”。 为了从语言设计与底层类型论的根基上化解这一裂隙，Cyrus 与其团队及合作者多年来探索了一系列方案。为了让观众有更切身的体验，他跳过对单篇学术论文细节的枯燥罗列，直接切换到了与该理念深度绑定的核心研究原型——**Hazel**（可在 `hazel.org` 体验的 Web 端自研编程语言与集成环境）。 --- ### [05:07](https://www.youtube.com/watch?v=fB_lklm7xgU&t=307s) Hazel 实机演示：编写 Quicksort Cyrus 调大 Hazel 网页终端的显示字号，进入草稿区（scratch mode），以计算机科学经典算法快速排序（Quicksort）为例展示系统特性。他首先按照严谨的测试驱动开发逻辑，使用 Hazel 的 `test` 关键字预置了针对快速排序的测试样例，随后开始书写主函数逻辑。 主函数匹配列表结构：当输入为空列表时，直接返回空列表；进入非空列表的递归分支时，算法将列表尾部（`tail`）针对选定的基准元素（pivot）进行划分，演示中直接选取表头元素（`head`）作为 pivot。Cyrus 幽默地插话道： > “Somebody once complained when I gave this demo that that's not quick sort if you just choose the head. But I think it's fine. It's Q sort.”（“之前我做这个演示的时候，有人曾抱怨说如果只选第一个元素当基准，那根本不叫快速排序。但我个人觉得无伤大雅，就叫它 Q sort 吧。”） 在写完前几行之后，整个程序处于明显的未完成状态，且同时暴露了两种截然不同维度的“不完整性”： 1. **语义未定义**：划分函数 `partition_at` 尚未实现，屏幕底部立即显式弹出常规静态反馈：“`partition_at not found`”。 2. **语法缺失**：在 `let... in` 表达式的 `in` 关键字之后，没有任何后续表达式。 在传统编程语言（如 OCaml、Rust 或 Haskell）中，缺少 `in` 后续体的代码将触发不可恢复的语法解析错误（Syntax Error）。一旦语法解析阶段崩溃，抽象语法树（AST）便无法生成，编译器甚至根本不会执行到类型检查阶段，上述关于 `partition_at` 缺失的语义诊断也无从谈起。 --- ### [06:19](https://www.youtube.com/watch?v=fB_lklm7xgU&t=379s) 类型孔洞、容错解析与实时探针 为根除传统解析器的全或无机制，Hazel 引入了一套由前博士生 David Moon（现供职于 Jane Street）参与构建的**容错解析器（error-recovering parser）**。系统认定 `in` 之后必然应当承载表达式，但它不会因缺失内容抛出致命错误，而是在该位置就地生成一个显式的占位符，即**孔洞（typed hole）**。 ```mermaid flowchart LR accTitle: Hazel 类型孔洞与动态探针工作流 accDescr: 展现容错解析器如何将不完整语法替换为六边形孔洞，并在孔洞未填补状态下通过探针观察局部执行数据。 A["代码输入：let... in （未完工）"] --> B["容错解析器（Error-Recovering Parser）"] B --> C["注入六边形孔洞（Hexagonal Typed Hole）"] C --> D["类型检查与运行时保持存活"] D --> E["挂载实时探针（Probe: Cmd+E）"] E --> F["捕获并显示真实输入数据：如 pivot=3, tail=[...]"] ``` 在 Hazel 的 UI 中，孔洞以独特的六边形图标呈现，文本光标也会贴合六边形的轮廓贴靠，展现出六边形块状解析结构。孔洞的引入让程序即使在语法残缺时也能顺利通过类型检查，使得“未定义标识符”与“语法待补全”两种层级的信息并存。 更具突破性的是其动态反馈能力：虽然实现尚未完成，开发者可以直接在任何表达式上挂载**实时探针（probe）**（通过快捷键 `Cmd + E` 或右键菜单触发）。在 `partition_at` 的调用点挂上探针后，即便该函数体完全不存在，屏幕右侧也会立刻反馈出该调用的实际运行时入参状态。 现场演示展现了探针捕获到的真实状态： - **模式匹配验证**：探针捕捉到函数正试图以数值 `3`（对应测试用例的首元素）以及剩余列表作为实参传入，证明上游的模式匹配解构工作完全正常。 - **多用例无缝切换**：底部的两个独立 `test` 样例驱动了不同的调用流，探针允许开发者直接在不同的调用栈帧（call instances）之间切换查看真实入参。 随后，Cyrus 开始着手定义 `partition_at` 函数，在现场询问观众近一个月是否有纯手动编码的经历，并在观众响应后继续展示 Hazel 在键入过程中的动态语法修复与六边形占位特性。 - **核心机制清单**： - **六边形孔洞（Holes）**：将未编写完成的代码或语法缺陷就地转化为具名的一级语言构造（first-class holes），阻断错误扩散。 - **动态探针（Probes）**：挂载于表达式上直接透视上下文中的实时运行环境与求值数据，无需插入 `print` 或设置断点。 - **测试用例驱动求值**：即使全模块处于包含未填补孔洞的非完工状态，现存的测试用例仍能部分求值并向探针注入鲜活数据。 ### [09:24](https://www.youtube.com/watch?v=fB_lklm7xgU&t=564s) 现场演示：编写分区函数与典型初学者错误 Cyrus Omar 继续在现场演示 Hazel 的实时编程功能，展示如何编写快速排序算法的核心辅助函数 `partition_at`。他首先对输入的列表 `xs` 进行模式匹配和情况分析（case analysis）：当输入为空列表时，划分得到的两个分区也都是空列表；而在头尾结构（head-cons-tail）的情况下，则需要考虑如何递归。他的目标是通过在尾部列表上以相同的基准值（pivot）进行递归调用，分别收集小于和大于基准值的元素。 在键入代码的过程中，Cyrus Omar 一度疑惑自己哪里写错了，随后恍然大悟：原来标准库中已经内置了一个同名函数 `partition`，因此他必须将其命名为 `partition_at`。修正命名后，他模拟了一个初学者非常容易犯的逻辑错误。对于模式匹配解构出的头元素 `hd` 与尾部 `xtail`，很多学生会下意识写下这样的比较逻辑：“如果基准值 `x` 小于头元素，就放到较小的一侧；否则放到较大的一侧。” ```mermaid flowchart TD accTitle: partition_at 逻辑演进流程 accDescr: 展示 partition_at 函数从错误实现到修正的两个步骤与实时反馈对比 subgraph Bug1["初次尝试：变量混淆错误"] A1["比较 x < hd"] --> B1["错误插入 pivot (x)"] B1 --> C1["实时探针显示: [3, 3, 3] ('Oops, all threes')"] end subgraph Bug2["二次修改：比较方向颠倒"] A2["修正插入 hd"] --> B2["保留 x < hd 比较"] B2 --> C2["实时结果：大小分区位置颠倒"] end subgraph Correct["最终修正"] A3["修改运算符为 x > hd"] --> B3["实时探针更新"] B3 --> C3["输出正确排序分区"] end Bug1 --> Bug2 --> Correct ``` - 在传统编程语言中，尚未写完的程序往往会直接报错终止，但 Hazel 允许不完整的语法和类型状态在编辑器中直接求值。 - 该函数在类型系统层面完全正确、没有任何类型错误，但业务逻辑本身存在偏差，传统静态类型检查器对此无能为力。 ### [10:52](https://www.youtube.com/watch?v=fB_lklm7xgU&t=652s) “哎呀，全是三”：利用实时数据排查运行时错误 代码刚写完，Cyrus Omar 便带领观众查看编辑器下方对 `partition_at` 的实时调用探针。屏幕上的求值结果让他忍俊不禁，当场惊呼：“哎呀，全是三！”（“Oops. All threes.”）。他向大家解释，自己在构建新列表时，把基准值变量 `x` 放进了列表的每一个位置，而不是原本应该放入的列表头元素 `hd`。 当他把 `x` 替换为 `hd` 之后，下方的求值结果瞬间实时刷新，显示出了真正来自输入的原始数据。Cyrus Omar 借此强调了 Hazel 的革命性差异：“如果是在传统编程语言中，这本该是一个语法解析错误；但我们让它越过了语法解析错误，越过了类型错误，一直推进到了编辑过程中的运行时反馈。”（“So, we've moved it past parse error, past type errors, all the way into runtime feedback while we're editing.”）。 然而，逻辑问题依然存在。台下观众敏锐地指出：“顺序反了。”虽然 Cyrus Omar 预期左边是较小的元素、右边是较大的元素，但实时渲染的数据清晰地显示，小元素全被排在了右边，大元素反而到了左边。这种基于真实 concrete 数据的即时反馈，彻底改变了编程体验：如果只是对着抽象的符号干瞪眼，开发者很容易漏掉这个细微的符号方向问题，最终得到一个完全倒序的列表。Cyrus Omar 随即把 `<` 改为 `>`，仅仅改动了一个字符，探针中的数据瞬间随之重算，两个分区立即恢复了正确的排列顺序。 ### [12:31](https://www.youtube.com/watch?v=fB_lklm7xgU&t=751s) 问答交互：纯函数性与副作用的隔离哲学 演示告一段落后，Cyrus Omar 打开现场提问环节，并开玩笑要拿传声麦克风砸向提问者。现场一位观众首先提问：在实时编辑求值时，如果程序陷入无限递归怎么办，开发者会被卡死吗？Cyrus Omar 回答称，系统不会阻塞用户输入；Hazel 的设计策略是在顶层函数调用遇到递归上限限制时，将该子表达式就地替换为一个 Typed Hole（类型孔洞），标明该计算在当前步数限制内无法算出，但周围的其他计算仍可越过它继续执行。 随后，另一位观众提出了一个直击 live programming 核心的痛点：“程序中的副作用该怎么处理？”（“What about side effects in programs?”）。Cyrus Omar 明确指出，Hazel 是一门纯函数式（pure）语言，不能直接在程序中随意执行网络请求或文件 I/O 等副作用。他解释道，由于环境在用户每一次击键（keystroke）时都会触发重算，如果不严格控制副作用，后果将不堪设想： > “如果你的程序正在进行交易，你总不会希望它在你每次敲击按键时都下一笔单，然后看着你的银行账户里发生什么吧。” > —— Cyrus Omar Cyrus Omar 说明，Hazel 在处理副作用的设计上更多借鉴了 Haskell： - 采用类似 Monadic I/O 的机制，在纯函数阶段仅仅构造出描述 I/O 行为的 Monad 数据值。 - 只有当开发者明确点击运行命令时，才会真正去执行纯函数阶段求值出的副作用。 ### [14:31](https://www.youtube.com/watch?v=fB_lklm7xgU&t=871s) 调用栈探查：多采样视图与调用帧下钻 现场观众针对测试与函数多次调用的渲染机制发起追问：如果一个函数被测试用例调用了多次，或者本身是一个深度递归函数，编辑器该如何呈现这些结果？Cyrus Omar 指出，在当前的屏幕演示中，下方的两个测试用例已经两次调用了快速排序函数 `qsort`。编辑器默认会采用折叠视图展示，用户可以通过滚动在多个采样结果间切换，或者双击并排展示多个采样值。 针对复杂调用栈的探索，Hazel 提供了内置的类似调试器的功能： - **测试关键字特性**：`test` 关键字并不是创造多采样的特殊语法，它只是在行内以小图标反馈断言结果。在函数未写完导致遇到孔洞终止时，测试状态会显示为一个问号。 - **抽屉式展开**：若求值结果数据过大，用户可以点击抽屉（drawer）图标展开面板，并配合 Shift + 拖拽自由调整视窗大小。 - **单步下钻（Step Into）**：对于包含多次递归或复杂调用的项，用户可以右键点击某个具体值并选择“Step Into”。这会将视重视图锁定到产生该值的单一样本上，不仅直接跳转至该调用的定义处，还会自动筛选并高亮该调用在调用栈下游派生出的所有样本。开发者借此可以精确定位到特定调用帧（call frame）中的中间局部变量状态。 ```mermaid flowchart LR accTitle: 调用栈样本探查与钉选流程 accDescr: 用户在 Hazel 中右键采样值并下钻单一样本的调用树交互 A["多次调用 / 递归求值"] --> B["默认折叠视图 / 多采样滚动"] B --> C["右键目标样本: Step Into"] C --> D["锁定特定父级调用 (Pinned)"] D --> E["自动过滤并高亮同属于该 Call Frame 的下游中间变量"] ``` ### [16:56](https://www.youtube.com/watch?v=fB_lklm7xgU&t=1016s) 孔洞的类型语义：符号化求值与渐进类型推断 随着讨论深入，观众开始关注 Hazel 核心的“孔洞（Holes）”机制。一位观众提问：孔洞可以被放置在代码的任意位置吗？如果把列表构造中的头部元素替换成一个孔洞，它会直接出现在运行结果中吗？这是否意味着系统支持“部分已知值（partially known values）”？ Cyrus Omar 当场在列表组装处插入了一个孔洞并演示求值，证实了这一猜想。他解释道，Hazel 在底层实际上是对孔洞进行**符号化求值（symbolic evaluation）**。孔洞并不是一个会抛出未实现异常（unimplemented exception）的中断指令，而是一个普通项（term），它会在程序求值流中顺畅传递，直到流转至无法继续分支消除的受阻位置（elimination position）才会暂停。 关于孔洞对类型系统的冲击，观众追问：“既然孔洞在 Hazel 中是一等公民，它们的精确类型语义是什么？因为孔洞过多可能导致类型根本无法推断。” Cyrus Omar 详细阐明了 Hazel 的理论基石： - **渐进类型（Gradual Typing）**：类型层面本身支持未知类型（unknown type，写作 `?`）。开发者既可以显式声明返回类型为 `List(?)`，也可以让不同分支类型冲突的条件表达式自动退化为未知类型。 - **类型孔洞推断（Type Hole Inference）**：系统在另一个独立分支中实现了基于合一算法（unification-style）的类型推断机制。推断器会竭尽全力求解合一约束；若无法完全求解，它会生成部分解（partial solutions），指出部分约束推导出的可能类型。一旦用户依据提示采纳某种填补选择，类型推断器就会基于该选择将错误精准局部化（error localization）到其他冲突位置。 - **运行时代价与工程权衡**：这种实时调试体验严重依赖解释器内部的内省（introspection）和追踪日志机制。对于小型程序而言运行极为平滑，但在超大型程序中记录全部调用帧数据开销巨大。因此，工程上必须引入采样上限策略（如在特定断点处只截取前 10 个样本）来维持交互的实时性。 ### [20:18](https://www.youtube.com/watch?v=fB_lklm7xgU&t=1218s) 采样解释器与执行性能 在开发如快速排序（quicksort）这类函数或进行数据分析时，开发者通常只需要处理形状匹配但规模较小的数据子集。针对这种场景，Hazel 采用了专门带有插桩（instrumented）支持的解释器版本，用于收集运行状态和探针样本。 关于性能权衡，当开发完成或函数接收到真实的大规模输入时，系统理想的做法是将其即时编译（JIT）为去除了调试插桩的高效执行代码。演讲者 Cyrus Omar 坦承： > “我们目前还没有构建那一部分，不过那也许可以是 OxCaml 之类的工具；目前这整个系统是用 OCaml 实现的。” ### [21:01](https://www.youtube.com/watch?v=fB_lklm7xgU&t=1261s) 探针颜色与多层调用栈（Call Frame） 观众就探针显示提出疑问：某些高亮为绿色的分支并没有在当前调用的顶层命中，如果输入一个空列表会发生什么？Cyrus 解释称，浅绿色代表代码被执行了，但不是在当前选定的调用帧（call frame）中，而是在其下游的基础情况（base case）里触发的。如果直接传入一个空列表，所有其他非空分支都不会产生采样数据。 针对递归函数（如 `partition_at`）重复调用时父子调用关系是否清晰的问题，Cyrus 展示了名为 **Probarium** 的侧边栏界面。该界面提供了红、绿、蓝三种颜色的调用栈上下文方案： - **蓝色**：表示该数据并非来自当前调用帧，而是位于调用栈下方更深处。 - **红色**：表示来自调用栈上层的上下文。 开发者可以直接“单步进入”（step into）特定递归层级来固定某一次调用，系统顶层会显示当前的调用栈深度（例如“深入 `partition_at` 两层”）。此外，系统也支持基于步数计数器（step counter）的时间旅行调试。针对复杂的递归，Cyrus 承认： > “对于递归，你最终会得到海量数据，如何在代码旁边以紧凑的 UI 形式将它们展示出来，目前仍然是一个开放性研究问题。” ### [24:30](https://www.youtube.com/watch?v=fB_lklm7xgU&t=1470s) 快速排序的闭环实现与快速反馈 完成快速排序的编写时，Hazel 的 UI（如背包设计 Backpack UI）提供了流式操作体验。开发者在对 `smaller` 和 `bigger` 两个列表递归调用 `quicksort` 时，系统甚至支持带动画的位置对调操作。 代码编写完成后，之前的问号占位符立即变成了绿色对勾（测试通过）。当演讲者故意将期望输出从 `[7; 9; 10]` 误写为 `[9; 7; 10]` 时，测试立即标红报错；一旦在代码中更正，测试结果毫秒级重算并变绿。传统编程流程要求写完代码后交由编译器等待数分钟，再在终端查看错误日志并手动回溯。对于这种模式，Cyrus Omar 评价道： > “我认为那整套折腾已经非常过时了，对于严肃对待即时反馈需求的编程体验而言，这才是更好的设计。” ### [26:09](https://www.youtube.com/watch?v=fB_lklm7xgU&t=1569s) 图形化表示法：从交互式表格到算法音乐 Hazel 的反馈机制不仅限于数字列表等纯文本输出，还内置了**图形化表示法**（Graphical Notation）系统，支持为任意类型自定义可视化展现形式： - **交互式数据表格**：在代码层面，表格由元组列表（list of tuples）表示，但在 UI 中直接渲染为排版规整的交互式表格。开发者在探针弹出的表格中点击下拉菜单按分数（score）降序排序，Hazel 会自动在底层插入由管道操作符连接的函数式排序代码（如调用 `int_compare` 等）。 - **算法声音与实时编码（Live Coding）**：系统支持将数据生成直接映射为算法音乐组件。底层代码虽只是数值，但在界面上直接渲染为底鼓（kick drum）选择器、军鼓（snare）、踩镲（hi-hat）、五线谱音符以及可点击发声的钢琴键盘。 - **旋钮与声相控件**：参数本质上只是数字，但由于“音乐人极度喜爱旋钮”，系统将滑块封装成了圆形表盘，探针不仅能在界面上绘出声波曲线，还能直接调用音频引擎播放合成的声音。 在演示现场播放由代码合成的节奏节拍时，暂停控件偶发故障导致音乐持续循环，引发全场笑声，Cyrus 幽默地自嘲： > “我想这就是我现在的宿命了吧。” 随后他关掉了该标签页。 ### [29:26](https://www.youtube.com/watch?v=fB_lklm7xgU&t=1766s) 转向智能体框架（Agentic Harnesses）与万级 Token 吞吐 当前软件工程范式正从人类手动编写代码，大规模转向由 AI 智能体框架驱动的环境。反馈回路的拓扑结构因此发生了深刻变化：除了传统的人机交互回路、人类开发者之间的协同回路外，新增了平行的“智能体-工具”反馈回路以及由多智能体组成的“蜂群”（swarms）。 ```mermaid flowchart LR accTitle: Human-AI and Tool Feedback Loops accDescr: Parallel feedback loops connecting human developers, AI agents, and their respective toolsets within a shared codebase. subgraph Humans["人类开发者层"] H1["人类开发者 A"] <-->|"同行评审 / 协作"| H2["人类开发者 B"] H1 <-->|"即时反馈 / 探针"| HT["人类编程工具"] end subgraph Agents["智能体蜂群 (AI Swarms)"] A1["AI 智能体 A"] <-->|"协同 / 交互"| A2["AI 智能体 B"] A1 <-->|"执行结果 / 类型反馈"| AT["智能体工具集"] end HT <-->|"共享代码库"| AT ``` 许多面向人类开发者的即时反馈设计理念，对于 AI 同样适用。尤其随着专用晶圆级 ASIC 硬件的研发，模型推理速度有望达到每秒 1000 个 Token 以上（远超当前前沿模型的数十至百 Token/秒）。当生成速度不再是瓶颈时，系统的性能瓶颈将直接转移到工具链本身。Cyrus Omar 强调： > “如果我们拥有这种每秒生成上千 Token 的 AI，我们完全可以预见，整个系统的瓶颈将会卡在工具自身——也就是智能体从系统中接收到的关于其操作的反馈回路之上。” ### [31:48](https://www.youtube.com/watch?v=fB_lklm7xgU&t=1908s) 智能体循环中的反馈瓶颈与“金鱼记忆”困境 在人与编程环境的交互之外，AI 智能体（Agent）自身的闭环循环也存在着非常严重的反馈延迟与高昂代价。现代前沿 AI 系统在语法错误方面犯错并不多，即使面对像 Hazel 这种在模型预训练数据中完全不存在的冷门研究型语言，智能体也能写出完全正确的语法。然而，类型错误（Type Errors）依然会导致编辑器服务的断裂——一旦代码中存在任何一处类型错误，整个运行时的反馈就彻底消失。这就把人类开发者面临的“工具服务断层”问题原封不动地移植到了智能体及其集群（Agent Swarms）身上。 不仅如此，AI 智能体还面临着独特的认知架构限制。Cyrus Omar 形象地打了个比方：“这些东西就像金鱼一样，每次启动一个新智能体，它就会把之前做过的一切忘得一干二净（these things are like goldfish, right? They forget everything they've ever done every time you start a new agent）。”因此，每当分配一项新任务时，系统必须快速向智能体灌入信息以重新建立上下文；而智能体在此过程中依然需要依赖编译器去执行代码、验证想法，漫长的重新编译与重新执行耗时，以及向模型输入海量纯文本日志所带来的高额 Token 与处理开销，构成了阻碍智能体自主迭代的严重瓶颈。 - **语法与类型表现**：模型很少犯语法错误，即使面对未见过的 Hazel 语言也能写对语法；但一旦出现类型错误，传统的运行时反馈就会全盘崩溃。 - **上下文冷启动负担**：智能体无跨会话记忆，极度依赖轻量、敏捷的即时反馈机制来进行上下文重建（Recontextualization）。 - **文本日志代价**：直接喂给 AI 庞大的纯文本终端构建日志既耗时又消耗巨额 Token。 --- ### [33:06](https://www.youtube.com/watch?v=fB_lklm7xgU&t=1986s) 细粒度增量性：从 AST 缓存到模式化记忆（Shortcut Memoization） 为了解决每一次微小按键都从头全量运行程序的性能浪费，Cyrus Omar 切回 Hazel 的实时演示界面，展示系统如何实现极高精度的“细粒度增量计算（Fine-grained Incrementality）”。在已经完成的快速排序（quicksort）代码中，系统已经内置了数条测试用例。此时新增一条测试，绝对不应该强迫系统去重新执行前面所有已经跑通的测试。 ```mermaid flowchart TD accTitle: Hazel Fine-Grained Incremental Execution accDescr: Shows how AST edits trigger partial re-execution while caching unchanged nodes and call paths. subgraph UserEdit["用户编辑阶段"] A["输入新测试用例或局部修改表达式"] end subgraph MemoAnalysis["增量分析与重用"] B{"AST 节点是否受修改影响？"} C["直接复用缓存值<br/>（界面高亮为蓝色无须重算节点）"] D["仅重算发生变化的表达式<br/>（如仅计算等式右侧求值）"] end subgraph AdvancedOpt["进阶优化：LA 2026 论文"] E["快捷记忆化（Shortcut Memoization）<br/>基于模式变量抽象的 Memo 表"] end A --> B B -->|"未受影响 (静态/动态)"| C B -->|"受影响局部"| D D --> E ``` 在开启可视化后，Hazel 编辑器中未受最新编辑影响的抽象语法树（AST）节点会高亮显示为蓝色标记。当 Cyrus Omar 现场键入一条新的等式测试时，Hazel 不仅直接跳过了之前全部测试用例的函数调用，甚至当他在该行写到一半、仅修改等式右侧时，系统检测到等式左侧的函数调用已计算完成，因而只对右侧表达式和外层的相等性判断执行重算。这种数据流分析和缓存不仅局限在执行层面，类型检查也同样是完全增量的（去年发表的相关语义论文已完成形式化正确性证明）。 针对更深层的代码逻辑微调（例如将递归分区中的 `x > head` 顺手改成 `x < head`），Cyrus Omar 剧透了他们即将发表在 LA 2026 上的新工作——**快捷记忆化（Shortcut Memoization）**。该机制利用带有模式变量（Pattern Variables）抽象的记忆表（Memo Table）来缓存中间计算结果。例如，只要系统观察到形如 `length(a:: b:: c:: nil)` 这种固定模式的列表调用恒等于 4，就能把这个模式抽象并缓存下来，搭配高度优化的查找数据结构，在函数体本身被修改后依然能够跨版本榨取最大的计算复用度。 > “构建系统通常是在编译单元（Compilation Unit）的粒度上来做增量化的；而我们一直在思考的，是在编程语言内部单个表达式的级别上实现这种增量性。” —— Cyrus Omar - **表达式级增量执行**：输入表达式的左侧求值完毕后，编辑右侧仅触发右侧与顶层比较运算的重新求值。 - **增量类型语义**：不仅仅增量判定整个文件是否类型正确，还能增量产生所有供编辑器底部探针渲染所需的中间类型信息。 - **Shortcut Memoization（LA 2026）**：通过模式匹配抽象记忆中间计算结果，跨越函数修改实现更深层次的计算复用。 --- ### [36:56](https://www.youtube.com/watch?v=fB_lklm7xgU&t=2216s) 为 AI 智能体打造原生结构化 IDE 针对 AI 智能体的开发工具链，核心设计思路不应停留在给 LLM 套上一层 Bash 终端外壳，而是要像对待人类程序员那样，为智能体量身打造实时的、增量式的语言开发环境。Cyrus Omar 介绍了 Hazel 的 AI 助手方案：它不同于基于纯文本行级 diff 或命令行交互的常规 Harness，而是直接运行在 Hazel 的**结构化动作语言（Structured Action Language）**与语义模型之上。该模型底层涵盖了带类型函数式程序、动态运行时探针数据，以及专门容纳未完成代码与类型冲突的“洞（Holes）”。 ```mermaid flowchart LR accTitle: Structured Agent Action vs Bash Agent accDescr: Contrasting standard Bash wrapper agents with Hazel's semantics-based structured action agent. subgraph StandardApproach["传统 Agent 范式"] B1["LLM 智能体"] -->|"低级文本命令 / 文本 Diff"| B2["Bash Shell 终端"] B2 -->|"易受同名函数干扰 / 吞噬大段日志"| B3["纯文本编译与错误输出"] end subgraph HazelApproach["Hazel 结构化范式"] H1["LLM 智能体"] -->|"结构化动作语言 AST Edits"| H2["Hazel 语义层 / 增量内核"] H2 -->|"精准定位唯一符号引用"| H3["语义搜索 & 跨作用域反查"] H2 -->|"行级内联实时数据流探针"| H4["实时结构化求值反馈"] end ``` 这种架构使智能体获得了人类级别的上下文辨识与外科手术式的修改能力：智能体能够直接执行语义搜索（Semantic Search）和语义上下文定位（Semantic Contextualization），即便工程中有大量同名函数，也能精确抓取到当前调用所对应的绝对定义。更关键的是，编辑区每行附带的实时内联数据流（Inline Feedback）可以直接序列化后喂回给模型，使智能体在敲完代码的瞬间就能核实流经变量的值是否符合预期，而无需堆叠到任务最后再去跑厚重的黑盒端到端测试。 初步实验覆盖了前沿 Frontier 大模型与中等参数量模型。结果显示，虽然模型几乎都是在 Bash 语料上训练出来的，但它们能够毫无障碍地理解并熟练调用这种丰富的结构化动作语言。由于智能体天生具有高度自我验证（Check their work）的倾向，这种“边写边验”的即时反馈极大降低了后期的排错负担。此外，得益于结构化编辑器支持精准的局部语法节点手术，模型无需一遍遍全量重写整段函数代码，这也显著减少了 Token 的消耗开销。 > “智能体可以在写代码的过程中就获得实时的内联反馈，去确认自己写的函数是否正确、流经其中的数据是否符合预期……它们非常喜欢这种即时验证的方式，就像人类也习惯边写边核对自己的工作一样。” —— Cyrus Omar --- ### [39:47](https://www.youtube.com/watch?v=fB_lklm7xgU&t=2387s) 人机协作瓶颈与叙事化变更导览（Narrativized Change Tours） 当开发流程转向人与智能体协作时，瓶颈往往卡在人类审查端。AI 的引入使每个人的代码产出速率与 PR（Pull Request）吞吐量暴增。Cyrus Omar 苦笑着坦言：“我不知道大家的情况如何，但我自己在各个项目里大概堆积了整整 50 个待审的 PR（I have you know maybe 50 open PRs in my various projects that I need to review）。”如果无法从审查端解放人类，整个研发链路的加速就会沦为空谈。 为了解决审查过载，Cyrus Omar 的团队与华盛顿大学（University of Washington）的 Hannah Potter 合作开展了一项名为**叙事化变更导览系统（Narrativized Change Tours）**的项目。该项目目前首先以 VS Code 插件的形式针对 GitHub PR 落地： - **变更文本块（Hunks）的故事线重构**：传统的 Git Diff 往往按文件目录树字典序或者散乱的修改次序罗列变更，而该系统要求所有 Diff 文本块串联成一个具备可读逻辑的故事（Narrative）。 - **详尽性检查（Exhaustiveness Checker）**：形式上是一个扩展 Markdown 文件，配套了静态检查器，严格保证 PR 中的每一个修改块（Hunk）都在叙事中被解释到，杜绝漏检盲区。 - **AI 技能辅助初始化**：借助 Claude 等大模型技能（Claude Skills）自动生成最初的导览叙事草稿，再由提交者或审查者润色。 在 Jane Street 现场交流时，这一设计引起了诸多工程师的共鸣。然而，Cyrus Omar 在结尾抛出了一个更为底层的架构危机：一旦数百上千个 AI 智能体同时在一个代码库上高频并发协作，现有的主流版本控制系统（如 Git）从底层机制上就根本不是为这种场景设计的，版本管理的瓶颈即将全面爆发。 - **PR 审查堰塞湖**：AI 工具的普及导致团队 PR 提交量远超人类 Review 的处理能力，评审成为工程吞吐的主瓶颈。 - **VS Code 开源插件**：目前该叙事化导览工具已封装为 VS Code 扩展供开发者与团队上手试用并参与实证研究。 - **并发协作极限**：数以千计的智能体实时对同一仓库进行细粒度并发编辑，传统的集中式或 Git 式分布式 VCS 已触碰承载力上限。 ### [41:32](https://www.youtube.com/watch?v=fB_lklm7xgU&t=2492s) 基于树型 CRDT 与 Unison 的大规模智能体协同编辑 在传统的开发工作流中，像“当前还有谁在编辑这段代码”这类问题，用 Git 是极难回答的。Cyrus Omar 指出，缺乏协同感知对 AI 智能体而言尤其致命，否则它们很容易陷入恶性循环：多个智能体同时修改同一处代码，产生冲突后各自以冲突的方式去解决冲突，进而又不得不去解决“冲突解决结果之间的冲突”。Cyrus 提到：“你甚至可能因为陷入这种死循环，为了构建某样东西而白白消耗掉 5 万美元的 Token。”他举了一个极具代表性的开源尝试：曾有团队试图利用 AI 智能体群构建一个从 JavaScript 到 WebAssembly 的形式化验证编译器，但由于智能体之间缺乏精细协调，所有智能体都本能地去抢最容易摘的“低垂果实”，在细微的代码风格层面互相冲突，最终烧掉了海量 Token 却没有产生多少实际成果。 为了从根本上解决这一问题，Cyrus 的研究团队（Future of Programming Lab）正在重新构建协同编辑的基础理论。去年他们开发了一套专门针对“树结构”而非“传统纯文本”的协同编辑系统。该系统基于结构化编辑动作，确保树上的编辑动作具备可交换性（commutativity），并在形式化层面完成了数学证明。其实质是一个面向树结构的图 CRDT（Graph CRDT for trees）。这套系统最关键的创新在于将“代码重定位”（code relocation，即代码移动）作为一等原生操作：在传统文本协同中，若一人将函数移动到 A 处，另一人将其移动到 B 处且有人对该函数做了修改，传统文本合并往往会直接复制出两份该函数，且完全不报冲突；而树型 CRDT 则能精准识别这类操作并合理处理冲突。 与此同时，他们还将这一研究与 Unison 编程语言的版本控制理念深度结合。在 Unison 中，代码永远不会从代码库中被真正删除，所有代码只增不减，变量与函数的引用全部通过内容寻址哈希（content-addressable hash）而非字面名称进行绑定。这意味着如果某个智能体定义了一个新版的 `List.map`，并不会立刻破坏现有的依赖代码，系统中只会并存两个版本的 `List.map`；开发者或智能体可以按需选择更新哪些调用点。对于并发生成海量实验性分支的 AI 智能体群体而言，这种机制允许它们并行探索、大胆尝试，之后再统一进行重构与清理，彻底摆脱了在大规模代码库上频繁全量重构的泥潭。 ```mermaid flowchart TD accTitle: 协同树编辑与内容寻址版本控制架构 accDescr: 展示从树结构CRDT原子操作到Unison哈希寻址与智能体并行演进的协同编辑流。 subgraph TreeCRDT["基于树的图 CRDT 协同层"] A["结构化树编辑动作"] --> B["代码重定位作为一等原语"] B --> C["具备可交换性 (Commutativity) 的合并"] end subgraph ContentAddressed["Unison 风格版本控制"] C --> D["内容寻址哈希引用 (Content Hash)"] D --> E["代码永不硬删除 / 允许多版本安全共存"] end subgraph AgentCoordination["智能体协作与维护"] E --> F["千级 AI 智能体并行分支开发"] F --> G["后期异步重构与清理通道 (Refactoring Pass)"] end ``` --- ### [44:32](https://www.youtube.com/watch?v=fB_lklm7xgU&t=2672s) 终结危险权限：基于对象能力的智能体沙箱架构 随后，Cyrus Omar 转向了系统的可信度与安全性问题。在智能体与环境深度交互的未来，面对敏感数据和高危系统调用，决不能直接赋予智能体操作系统的 root 权限甚至普通终端访问权。现场爆发出笑声，因为 Cyrus 调侃了当前很多开发者的不良习惯：他在使用各类辅助编码工具时，为了省事常常随手打开“危险地跳过权限确认”（dangerously skip permissions）这一选项，引得台下会心一笑。对此 Cyrus Omar 幽默地反思道：“‘危险地跳过权限’——我真怀疑这到底危不危险。” ```mermaid flowchart LR accTitle: 基于对象能力的权限衰减模型 accDescr: 根权限通过对象API层层衰减为专用受限能力，并交由证明助手与监督者验证。 RootCap["根级权限能力<br/>(例如：通用 File I/O)"] AttenuatedCap["衰减后的能力<br/>(例如：仅追加的 Log 权限)"] Agent["执行特定任务的 AI 智能体"] FormalProof["形式化证明助手<br/>(证明信息流控制安全策略)"] RootCap -->|"权限衰减 (Attenuation)"| AttenuatedCap AttenuatedCap -->|"注入任务上下文"| Agent FormalProof -.->|"约束验证"| AttenuatedCap ``` 为了彻底消除这一安全隐患，Cyrus 主张将软件架构中的经典概念——对象能力（Object Capabilities）引入智能体工具语言的设计中。在对象能力模型中，系统的外部副作用被封装在微小的对象 API 中，且语言在底层保证能力指针不可伪造： - **能力衰减（Capability Attenuation）**：系统根组件即便拥有完整的文件 I/O 权限，也可以将其衰减为一个仅支持“向特定日志文件执行追加操作”的单向能力对象。 - **最小权限原则**：当该衰减对象被传递给负责写入日志的智能体时，该智能体物理上无法突破该能力去执行任意格式化、读取其他文件等越权操作。 - **可证明基线与信息流控制**：团队在 HOPE 车库会议（Workshop on Higher-Order Programming with Effects）发表的论文中探讨了如何借助交互式定理证明助手，形式化证明安全基线策略的正确性。他们还与医疗隐私领域的专家合作，通过在工具语言中内建信息流控制（Information Flow Control），形式化证明敏感数据（如病人的电子邮件内容）绝对只流向该病人自己的病历卡，而决不可能泄露到任何其他病人的档案或外部邮件通道中。 --- ### [47:02](https://www.youtube.com/watch?v=fB_lklm7xgU&t=2822s) 未来愿景：像维基百科般运转的“动态计算公域”与现场问答 在演讲的总结部分，Cyrus Omar 描绘了这一系列研究的终极愿景：“动态计算公域”（Live Computational Commons）。他认为未来不应是碎片化的独立代码仓库，而应是一个由海量 live 程序紧密互联构成的执行网络，其核心特征包括： - **人机共生与非专业者协同**：平台同时支持成千上万的人类和 AI 协同修改。对于大量非程序员，界面将计算结果转化为动态报告、图表或音频等实时可操作组件；AI 在编写绘制柱状图的代码时，如果不知道柱条的精确宽度，可以主动在界面上留出一个动态滑块（Live Literal Slider），交由人类监督者直接拖拽调整。 - **全系统容错韧性**：如同维基百科一样，哪怕某个用户或智能体在某一页引入了语法错误或类型错误，也仅局限为局部的类型孔洞（typed hole），绝不会导致整个公域系统瘫痪崩溃。 - **模块化与细粒度增量重算**：每个页面在语义上相当于一个 OCaml 风格的模块，任何局部的编辑操作只会触发下游真正依赖该值的极小范围增量重算。 - **应对现实世界建模挑战**：Cyrus 提到他组织了一场名为“Programming for the Planet”的气候科学研讨会，并计划前往剑桥大学进行为期一年的学术休假（sabbatical），与顶级气候科学家合作将这套系统付诸实践——将鱼类生态模型、海水温度模型、冰盖运动模型等异构模拟器整合进统一的、活态的计算公域中，让它们作为活程序互相通信，而非死板的数据集。 演讲结束后进入提问环节。第一位提问的观众立刻提出了尖锐的质疑：提问者表示，其实业内现在就已经有类似模式在良好运转了——比如在他们公司内部（暗示 Jane Street），就有数千名开发者在一个庞大的单体代码库（Monorepo）中高频交互，大家各自提交修改、合并冲突，偶尔需要 rebase，但整套体系目前运转良好，似乎并没有 Cyrus 所说的那么不可行。面对这一挑战，Cyrus 坦承自己的说法可能有些绝对，但他随即指出，现有机制在超大规模和极高验证要求下已经开始“发出不堪重负的吱吱嘎嘎声”（starts creaking）。为了佐证，他提到了近期与 Lean 定理证明社区以及庞大的 Mathlib 数学形式化库开发者的深入交流，而那正是当前计算公域面临协作瓶颈的最前沿阵地。 ### [51:03](https://www.youtube.com/watch?v=fB_lklm7xgU&t=3063s) 智能体协作的细粒度与 Git 基础设施的演进 观众与 Cyrus Omar 探讨了 AI 智能体在高频编辑下的协作范式。传统编译器和基于 Git 的工作流难以适应这种极高频率的变动，因为“智能体进行的编辑操作实在太多、太快了”。当大量智能体同时在证明与当前任务相关的引理时，如果必须等待对方完成证明并提交（commit），就会产生严重的协作脱节。智能体往往希望在引理被正式提交之前就感知到其他智能体的进度。针对这一场景，Cyrus 澄清说，他并非主张抛弃现有的版本控制基础设施，而是设想一种混合形态： “我心里想的更偏向于 Google Docs 那种风格——你能看到光标在屏幕上穿梭移动，但底层依然保留着 Git 风格的基础设施；而不是把一切推倒重来、搞得好像我们根本不知道怎么做协作一样。” 观众提问进一步聚焦于粒度（granularity）是否是核心转变。人类开发者已有成熟的工作分解和沟通习惯（例如配合使用 Google Docs 与特性分支），那么当细粒度协作扩展到超大规模时会发生什么？Cyrus 回应称，即便没有极端细粒度的支持，大规模工程同样在运转；但随着越来越多的智能体在同一组组件上进行快速迭代，这种细粒度的重要性会呈指数级上升： - **组件隔离与传统视角**：如果系统具备良好的架构边界，且单一组件内同一时刻只有一两个智能体在工作，那么传统的开发协作模式依然有效。 - **引用历史版本的能力**：在单一片上代码库（codebase）中直接引用旧版本，避免在像 opam 等包管理器做版本解析时被迫强制锁定在单一规范版本（canonical version）。Unison 语言在此方面奠定了坚实的基础。 - **精确跟踪代码位置迁移**：相比 Git 基于启发式的文本比对，能够正确、原生处理代码重定位（code relocation）的原语至关重要。 ### [53:47](https://www.youtube.com/watch?v=fB_lklm7xgU&t=3227s) 形式化数学证明与跨学科的“计算公域” 现场观众提问，这种大规模协作形式是否已被应用到数学研究和形式化数学证明（formal proof）中。Cyrus 坦言，其实验室目前尚未在任何领域完整落地超大规模协作，工作重心仍在筑牢基础原语。但在定理证明方向上，Hazel 团队正积极推进新功能集成： “我们正在为 Hazel 添加定理证明器的能力；实际上，我们更多是基于 Isabelle 风格的设计，而不是像 Lean 那样采用依赖类型、全谱系依赖类型的设计。” 针对形式化证明在未来的角色，Cyrus 提出了几点研判： - **证明成本的结构性转变**：过去形式化验证需要顶尖专家耗费巨额时间编写，如今随着大语言模型和相关工具的发展，可以直接让底层工具尝试自动求解证明，大幅降低了验证门槛。 - **代码审查范式的革新**：未来的代码审查将变得更抽象——开发者不再需要死抠具体实现细节，而是审查“这些不变量（invariants）定义得是否有意义”，随后只要系统验证了对应不变量的正确性证明，整套逻辑便可安全合入。 - **破除工具壁垒的统一公域**：长期以来，数学、自然科学和工程技术分别依赖互不通约的工具集；将它们统摄在同一个基于类型论的计算公域中，能够促成跨领域的直接协作与复用。 ### [55:14](https://www.youtube.com/watch?v=fB_lklm7xgU&t=3314s) 大规模状态管理与外部数据接口（FDI） 一位观众抛出了关于“状态（State）”的核心疑问：当众多计算笔记本或节点同时操作超大规模的数据集时，数据究竟存储在哪里？尤其是在类似“Planet Hazel”的公域构想中，如何承载物理世界的海量数据。 Cyrus 解释称，概念上整个计算公域模型就像一张“巨大的电子表格（giant spreadsheet）”，理论上数据与计算共同存在于表格之中。但面对真实世界中行星级（planetary scale）的数据集，数据不可能完全加载到本地 IDE 的内存里。为此，团队正在构建一个名为“外部数据接口”（Foreign Data Interface, FDI）的系统： ```mermaid flowchart LR accTitle: FDI 架构数据下推流程 accDescr: 展示用户在 Hazel 中编写纯函数变换，经过 FDI 转化为 SQL 并推送到 Spark 或远程数据仓库执行的过程。 subgraph HazelIDE["Hazel 环境 (IDE)"] direction TB Code["用户声明式代码<br/>(纯函数式变换 / 过滤)"] FDI["外部数据接口 (FDI)<br/>运行时可拔插组件"] Code --> FDI end subgraph RemoteStore["远端数据基础设施"] direction TB Spark["Apache Spark / JIT 引擎"] SQLStore["远端 SQL 存储 / 数据仓库"] Spark --> SQLStore end FDI -->|"下推 API (Push-Down API)<br/>将过滤/变换转为查询调用"| Spark ``` - **FDI 概念类比**：类似于程序设计中的外部函数接口（FFI），FDI 专门用于衔接外部异构数据集。 - **借鉴 Apache Spark 的算子下推**：受到 Spark Push-Down API 的启发，开发者在 Hazel 中编写纯函数式的数据过滤与变换，FDI 运行时能够将这些操作下推转化为底层的 SQL 调用或远程存储引擎原生操作。 - **针对大数据集的 JIT**：系统计划针对海量数据集提供面向 Spark 的即时编译（JIT to Spark），兼顾上层纯函数语义与底层分布式数据引擎的高效吞吐。 ### [56:56](https://www.youtube.com/watch?v=fB_lklm7xgU&t=3416s) 类型论本体、嫉妒驱动的研究与视觉化表示 现场观众提问，Hazel 将代码结构化为语法树而非纯文本流，这种高度固化的意见（opinionated view）在推向更广泛的开发者社区时，究竟能产生多大范围的约束力。Cyrus 阐述了他对软件本体论（ontology）及科研影响力的看法。他指出，采用树状表示的核心并不是对“树”本身的偏执，而是坚信类型论是构建知识和系统体系的最佳基石： “如果说我有什么强烈的观点，那就是计算公域应当植根于乘积类型（products）、和类型（sums）、函数（functions）以及模块（modules）之上。” Cyrus 将此与 2000 年代初语义网（Semantic Web）提出的资源描述框架（RDF）进行了对比。RDF 试图把所有知识都建模为无类型实体之间的二元关系，而现实世界充满非二元关系与多样化的类型区分，因此基于类型论的本体论远比 RDF 更合理。谈及对工业界和外部世界的影响力时，Cyrus 幽默地分享了自己的学术指导哲学： “我在我们组里推行转化研究的理念，其实就是‘通过嫉妒实现转化’（translation by jealousy）。” - **通过嫉妒实现转化**：团队致力于打造出兼具美感与严谨数学证明支持的原型工具；一旦做到了极致，便会激发其他技术社区的“嫉妒心”，促使外部开发者模仿并落地类似理念（例如将富图形整合进代码、带类型孔洞的编程等）。 - **纯粹性与实时求值分析**：若语言不具备纯粹性（purity），在每次击键时都运行完整程序是不切实际的。但这可以通过最佳努力（best-faith）策略来缓和——例如接受潜在副作用，或者引入语义分析进行浅层纯度检查（正如 Chrome 开发者工具对 JavaScript 进行保守分析后支持安全表达式的实时求值）。 - **界面美学与设计力量**：在回应观众对 Hazel 视觉美观度的赞赏时，Cyrus 将功劳归于团队成员（包括 David 以及另一位合作者 Andrew Blinn 等），肯定了优秀设计师将代码转化为表格、图形化界面的关键作用。 ### [01:01:12](https://www.youtube.com/watch?v=fB_lklm7xgU&t=3672s) 代码概念的重塑与技术栈更迭的成本变革 在问答环节，一位观众提出了一个极具哲思意味的问题：随着图形化、滑块控制以及智能体集群在共享代码库中自主修改代码的设想逐步成为现实，人类对“代码”本身的认知可能会发生根本性偏移。过去，代码本质上就是存储在文件里、最终被送去编译的一串文本；而当系统变得越来越抽象，底层技术栈层层叠叠时，人类还能理解这层层堆叠之下的底层细节（“how much will humans understand what all the turtles that are underneath?”）吗？ Cyrus Omar 对此回应称，人类是否能完全理解底层的“乌龟”尚未可知，但更关键的问题在于：在构建新系统时，我们是否还需要继续沿用过去那套早已固化的底层积木。他指出，随着大模型和自动化工具的普及，构建新语言生态与采用新技术的成本结构已经发生了天翻地覆的剧烈变化。 过去，推出一门新编程语言最大的阻碍在于极其高昂的生态建设成本——需要花费数亿美元的工程资源去撰写标准库、建设周边生态并对抗既有语言的强大网络效应。但 Cyrus 指出，如今的现实已经完全不同：“现在，我只要让 Claude 跑上一个通宵，就能为 Hazel 生成我想要的任何库。”他的团队甚至能够轻松将其他语言的代码直接移植到 Hazel 中，比如将各种 Jupyter Notebook 转换成 Hazel 原生笔记本，用作数据分析案例。因此，他呼吁计算机科学界应当抓住这个历史机遇，大胆去重新设计未来的正确形态，而不是被动地继续在陈旧的基础设施上修修补补。 > “我觉得现在的成本结构已经变了，我认为这正是我们计算机科学家群体去思考‘未来应该是什么样’的大好时机。” —— Cyrus Omar - **开发成本重构**：大语言模型（如 Claude）支持自动化生成代码与标准库，大幅降低了新兴语言的生态冷启动门槛。 - **跨生态快速迁移**：Hazel 研究团队已实现将外部数据科学代码（如 Jupyter Notebook）低成本迁移为基于类型孔洞与动态反馈的 Hazel Notebook。 - **挣脱网络效应束缚**：开发者不再必然被束缚在耗资数十亿美元建立起来的旧基础设施上，行业迎来了重新设计编程语言基石的窗口期。 --- ### [01:03:12](https://www.youtube.com/watch?v=fB_lklm7xgU&t=3792s) “一切皆实时”之下的部署概念与 Unison 哈希寻址方案 随后，另一位现场观众对这种持续演化、高度动态的实时编程环境提出了质疑：如果整个环境每分每秒都在变化、各类主体都在与它即时交互，那么“开发中的代码”与“已部署的代码”之间的传统界限是否彻底消融了？在这样的世界里，“部署”（Deployment）到底意味着什么？又该如何确保实时的改动不会立即破坏依赖者的生产环境？ Cyrus Omar 坦承自己处于一种“矛盾的心态”（two minds）之中。从一方面看，他本能地对“一切始终处于实时运行”（everything is live all the time）所带来的混沌状态感到兴奋。例如在气候科学领域，全球数以百万计的传感器每毫秒都在产生全新读数，卫星每天都会传回地球表面每 10 平方米的遥感数据。在这样的应用场景下，如果每次想要获知地球当前的综合状态或验证某项政策干预措施的推演结果，都必须等待气候模型花上整整两年时间发布一次大版本更新，效率将极其低下；此时，能够实时吸纳数据、持续重估的动态计算环境就具有巨大的现实价值。 然而在另一方面，针对严肃的通用软件工程，Cyrus 承认人类确实需要稳定性，绝不能容忍代码在毫秒级无序突变。针对这一挑战，他将解决方案指向了 Unison 项目的设计思想。Unison 抛弃了传统“文本文件 + 路径版本”的做法，对代码中的每项定义都采用基于抽象语法树的内容哈希（Content Hash）进行寻址。在这套机制下，旧版本的定义由于哈希固定，会永久保存在系统中；任何新代码的更新与旧引用的迁移都必须经过显式而严谨的重构流程。Cyrus 强调，尽管技术上他们正在借助类似 Unison 的机制为 Hazel 打造稳健的基础设施，但工程团队内部清晰的沟通机制、决策流程和组织规范依然不可或缺。演讲在现场观众的热烈掌声中落下帷幕。 > “在气候科学的背景下，我们每毫秒都会从遍布全球的数百万个传感器接收新数据，卫星每天也都会采集地球上每 10 平方米的新数据；如果我们不必在大型气候模型的各个小版本发布之间苦等两年，那该有多好。” —— Cyrus Omar ```mermaid flowchart TD accTitle: 实时计算模式与 Unison 确定性部署模式对比 accDescr: 展示了实时动态计算（如气候数据推演）与基于 Unison 语法树哈希引用的不可变部署架构之间的技术差异。 subgraph LiveMode["实时动态模式（数据流驱动）"] S["全球传感器 & 卫星数据"] -->|"持续写入"| Core["实时动态计算核心 (Live State)"] Core -->|"即时反馈"| Policy["政策推演与实时观测"] end subgraph UnisonMode["工程确定性模式（Unison 风格机制）"] V1["旧版本定义\n(固定 AST Hash: #abc1)"] V2["新版本定义\n(生成新 AST Hash: #xyz9)"] V1 -.->|"永不隐式覆盖"| V2 Client["依赖方应用"] -->|"显式决议 / 静态锁定"| V1 Client -.->|"团队受控迁移"| V2 end ``` - **高频数据推演的实时需求**：气候科研场景下全球百万级传感器每毫秒更新、卫星每日全覆盖扫描，传统数年一更的模型交付模式无法胜任实时干预推演。 - **Unison 的内容寻址方案**：代码不再是纯文本，而是拥有唯一哈希身份的语法树节点。历史版本永不丢失，避免了代码隐式更新引发的“破坏性级联故障”。 - **组织流程不可替代**：形式化技术工具虽然解决了底层的依赖稳定性，但系统何时升级、如何同步推进，依然依赖团队严密的工程治理与决策。 ## Notable quotes > [29:26](https://www.youtube.com/watch?v=fB_lklm7xgU&t=1766s) 如果我们拥有这种每秒生成上千 Token 的 AI，我们完全可以预见，整个系统的瓶颈将会卡在工具自身——也就是智能体从系统中接收到的关于其操作的反馈回路之上。 — Cyrus Omar > [56:56](https://www.youtube.com/watch?v=fB_lklm7xgU&t=3416s) 计算公域应当植根于乘积类型（products）、和类型（sums）、函数（functions）以及模块（modules）之上。 — Cyrus Omar > [12:31](https://www.youtube.com/watch?v=fB_lklm7xgU&t=751s) 如果你的程序正在进行交易，你总不会希望它在你每次敲击按键时都下一笔单，然后看着你的银行账户里发生什么吧。 — Cyrus Omar > [33:06](https://www.youtube.com/watch?v=fB_lklm7xgU&t=1986s) 构建系统通常是在编译单元（Compilation Unit）的粒度上来做增量化的；而我们一直在思考的，是在编程语言内部单个表达式的级别上实现这种增量性。 — Cyrus Omar ## Mentioned Jane Street, Cyrus Omar, David Moon, Hannah Potter, Andrew Blinn, Hazel, Unison, Grove, OCaml, OxCaml, Haskell, Rust, Lean, Mathlib, Isabelle, Apache Spark, Claude, VS Code, GitHub, Jupyter Notebook, WebAssembly, JavaScript, Google Docs ## Video description Rooted in Cyrus Omar's group's work on the Hazel live programming environment, this talk presents a vision for a "live type-theoretic computational commons": a shared monorepo where humans and swarms of AI agents make verifiable progress on parallel coding tasks. The collaboration model combines novel editing primitives (e.g. CRDT-based structure editing and Unison-style versioning) with familiar type-theoretic structure (e.g. OCaml-style modules and interfaces, Isabelle-style proofs). Two research problems take center stage. First, large-scale collaboration requires that incomplete programs remain continuously analyzable and executable — Cyrus will present recent foundational work on live, incremental type checking and evaluation of programs with typed holes. Second, as agent swarms grow in size and ambition, giving them direct terminal access to our machines and data becomes more risky. He will present a type-theoretic object-capability architecture that provably bounds agent behavior, with per-task capability signatures shaped by humans and weak AI supervisors to enforce the principle of least authority. 00:00:00 – Feedback loops, from pianos to compilers 00:03:29 – The gap problem in dev tools 00:05:07 – A live demo of Hazel: writing quicksort 00:06:19 – Holes, error recovery, and live probes 00:10:14 – "Oops, all threes": debugging with real data 00:12:42 – Demo questions: purity, holes, and call frames 00:25:56 – Graphical notation: tables, dials, and music 00:29:26 – Agentic harnesses and swarms of agents 00:33:33 – Incrementality: re-execution and type checking 00:36:56 – Live incremental IDEs for AI agents 00:41:19 – Collaborative editing for thousands of agents: Grove and Unison 00:44:32 – "Dangerously skip permissions" and object capabilities 00:47:02 – A live computational commons, from Wikipedia to climate models 00:50:24 – Audience Q&A [Source](https://www.youtube.com/watch?v=fB_lklm7xgU)

[29:26] Cyrus Omar: 如果我们拥有这种每秒生成上千 Token 的 AI，我们完全可以预见，整个系统的瓶颈将会卡在工具自身——也就是智能体从系统中接收到的关于其操作的反馈回路之上。 [56:56] Cyrus Omar: 计算公域应当植根于乘积类型（products）、和类型（sums）、函数（functions）以及模块（modules）之上。 [12:31] Cyrus Omar: 如果你的程序正在进行交易，你总不会希望它在你每次敲击按键时都下一笔单，然后看着你的银行账户里发生什么吧。 [33:06] Cyrus Omar: 构建系统通常是在编译单元（Compilation Unit）的粒度上来做增量化的；而我们一直在思考的，是在编程语言内部单个表达式的级别上实现这种增量性。

[36:56] Cyrus Omar: I think the way to think about it is that we need to build good live incremental IDEs for AI agents just as much with the sort of the same design thinking that we put into tools for human programmers.

[0:00] Right. Hi everyone. Uh thank you for uh [0:02] coming. Thank you for having me here at [0:04] Jane Street. So I'm I'm really excited [0:05] to talk about this kind of very uh big [0:08] picture vision for the future, but I [0:09] really kind of want to build up from um [0:12] the uh the simpler past that we've [0:14] inhabited for the past many decades um [0:17] before we get there sort of towards the [0:19] end of the talk. Um so if I sort of I [0:22] was thinking about kind of what what [0:23] some of the themes are in in this talk [0:25] and in my research in general. Um and I [0:28] think kind of a big theme for me is I [0:30] think a lot about feedback loops. Um and [0:32] actually even before I started working [0:33] in programming languages, I was thinking [0:35] about feedback loop fe feedback loops in [0:37] the brain. I did some information [0:38] theory, feedback information theory. Um [0:41] um but uh about uh 15 years ago, I [0:44] started really thinking about this very [0:46] basic feedback loop. We are humans and [0:48] we're using tools. We provide [0:51] information to the tools. We drive them [0:52] and the tools provide us feedback. Um [0:55] and I mean this in a very general way. [0:57] Many different kinds of tools um sort of [1:00] are have been designed uh in order to [1:02] provide good feedback. And what is good [1:04] feedback? It's uh there's many qualities [1:06] to good feedback, but certainly we want [1:08] feedback that's timely. We want feedback [1:10] that's not too ownorous for us to [1:12] process, right? Um I think this is very [1:15] intuitive. There's also lots of [1:16] behavioral science research to back up [1:18] uh back up this claim. Um if you think [1:20] about kind of the the tools that we used [1:22] before computers um we used to play [1:25] music together. We used to paint people [1:28] playing music. Um and uh these are these [1:32] are tools paint brushes in you know [1:34] pianos instruments where the feedback is [1:36] extremely timely. Right? As soon as you [1:38] press a key on the piano you get that [1:40] you hear the the the um the note that [1:42] was played. As soon as you lay a brush [1:45] onto a piece of paper you get uh [1:47] feedback about uh where the ink is [1:48] lying. um and we process it very quickly [1:52] as humans, right? Our sensory our [1:54] sensory organs are able to uh to hear [1:56] and see and these kinds of things the [1:58] feedback um as soon as it's available. [2:01] So so this is great. This supports uh [2:03] learning um quickly. It supports uh [2:05] really kind of uh the the upper bound of [2:09] of performance for this kind of thing. [2:11] I'm sure you've seen in in uh in the [2:14] world, right? Very very very high. Um, I [2:18] want to think of a hypothetical where [2:20] that weren't the case, right? Imagine [2:22] you're learning to play piano, right? [2:24] And you press a key and you don't hear [2:26] the note. Instead, you have to keep [2:29] pressing keys for a while to complete [2:31] the song. And you'll hear the song if [2:35] you played it completely correctly. [2:37] [laughter] [2:38] But if you made one wrong move in that [2:40] in that song, you won't hear it at all [2:42] and it'll just give you an error. [2:47] And also, you won't get that error for [2:48] about 3 minutes afterwards. [2:51] Well, that's kind of what uh the [2:53] state-of-the-art is in computer [2:55] programming. And we've kind of accepted [2:56] this, right? So, uh when we learn to [2:58] code, we kind of just kind of type for a [3:00] while and then we hit the compiler and [3:02] we ask it, did I do it all correctly? [3:04] And it says no. And then we go back and [3:07] we we work without feedback for a while [3:09] and then we ask again and eventually we [3:11] we kind of figure it out. I think it's [3:13] kind of amazing that humans can code at [3:15] all. Um, but uh we've managed to uh [3:18] improve on on on sort of the timeliness [3:21] and and the the u the modality of the [3:23] feedback over time. You know, modern [3:25] tools of course you're getting things [3:26] like syntax highlighting as you go. So [3:28] it's not all delayed, right? But [3:29] certainly any dynamic information about [3:31] this program, you can't run it if you [3:33] have any syntax errors, if you have any [3:34] type errors, uh you're not getting any [3:36] feedback about even the parts of the [3:37] program that are sort of finished. And [3:39] so I think that's that's kind of sad. [3:42] And so um a lot of the work that I've [3:44] been doing over the past uh many years [3:46] has been focused on this problem of [3:49] feedback in dev tools being kind of [3:50] delayed and difficult to process in [3:52] various ways. Um more specifically um [3:57] one of the big problems that I've been [3:58] thinking about is this this problem I [4:00] call the gap problem. Syntax and type [4:02] errors and other kinds of errors cause [4:04] uh gaps in the sort of editor services [4:06] that you want. Um you know go to [4:08] definition if there's type error [4:09] anywhere maybe it doesn't have that [4:11] information. available for you to go to [4:13] it. Um, but also just kind of natural [4:15] things in in computer programming. [4:16] Compilation times and recompilation [4:18] times every time you make an edit can be [4:20] long. Uh, programs can exe take a long [4:23] time to execute or re-execute even if [4:24] you make a small change. Um, and then [4:26] the output that you get is often not uh [4:29] quickly or easily processed by our our [4:31] human sensory organs. You get large [4:32] textual logs that you have to go and [4:34] parse. Okay. Okay. And so I've been [4:36] doing a lot of different um projects to [4:38] to with with various students, [4:39] collaborators on um on all these [4:42] different um areas. Um instead of going [4:45] into kind of depth about the the [4:47] research results in each of them, I'll [4:48] just kind of flash some of the papers in [4:50] the you can go look at the the video [4:52] later and and look some of these up. [4:54] What I really want to do is um show you [4:56] some of this stuff in the context of a [4:58] demo. So I'm going to um demo Hazel. [5:00] What Hazel is is it's a um it's kind of [5:03] a research envir a programming [5:05] environment and a programming language [5:06] that was co-designed. Um it's web based [5:08] so you can go to hazel.org and play with [5:09] it yourself. Um and it's it's kind of [5:11] motivated by this problem of rapid and [5:13] and um easily processed feedback. Let me [5:17] go and switch over to that. [5:22] Okay. So I've opened up Hazel. Is this [5:24] big enough? A little bigger. People in [5:27] the back seat. Okay. Great. So, um I'm [5:31] just in in scratch mode in Hazel and [5:34] I've started working on a classic [5:36] problem in in computer science curricula [5:39] called quicksort, right? And so I'm [5:41] doing the um the right thing here. I've [5:43] written some tests initially of [5:46] quicksort using this test keyword in [5:47] Hazel. And then I've started writing the [5:49] quicksort function. Um so I've you know [5:52] I've handled the base case where if the [5:54] list is empty then well I just return a [5:56] sorted list. And then what I want to do [5:58] is I want to really implement the [6:00] quicksort algorithm. So in the recursive [6:01] case, what I'm going to do is first I'm [6:03] going to partition um the tail of the [6:05] list against a pivot element. And that [6:06] pivot element I'm just going to for [6:08] simplicity choose here to be head. [6:10] Somebody once complained when I gave [6:12] this demo that that's not quick sort if [6:13] you just choose the head. But I think [6:16] it's fine. Okay. [laughter] Uh [6:20] it's Q sort. All right. So what I've [6:23] done so far is I've written you know a [6:24] bit of this program but it's incomplete. [6:26] It's incomplete in two ways. So one is [6:29] this partition at function hasn't been [6:30] written yet. And so you get kind of an [6:32] error here in the usual way. You can see [6:34] at the bottom of the screen here, [6:35] partition at not found. So it's giving [6:37] you that kind of static feedback that [6:39] you would expect. Um this is a little [6:41] bit more of a an an an interesting form [6:44] of incompleteness. Right? So I haven't [6:46] actually written anything after the in [6:48] keyword in my let in. Um in a [6:50] conventional programming system, this [6:51] would actually be a syntax error. Right? [6:53] If you just write let in and then you [6:54] end your in your program, it's not going [6:56] to and your function is not going to be [6:58] happy. It's going to give you a syntax [7:00] error. In fact, it won't then give you [7:02] that type error that you see above [7:03] because it has to go through the parser [7:05] even to get to the type checker. And so [7:07] in Hazel, we don't do that. In Hazel, we [7:09] instead um have an error recovering uh [7:12] parser uh actually built by David Moon [7:15] here. He's now James Streeter. Uh he was [7:17] a PhD student in my group. Um, so, uh, [7:21] what it does is it says, well, there [7:23] must be some there there needs to be [7:25] something here. There needs to be, uh, [7:27] an expression after the in. And so what [7:28] I'm going to do is I'm going to recover [7:30] from that syntax error, not by creating [7:32] by by just leaving an error, but by [7:34] actually, uh, putting in an explicit [7:36] placeholder called a hole in the [7:38] program. And holes are these little [7:39] little hexagons. And you can see our [7:41] carrot and hazel actually follows the [7:43] shape of the hexagons. Um, so you can [7:46] see that it's kind of this this [7:47] hexagonal block structure in the in the [7:50] parser. Okay. So, so far so good. So, [7:54] what I want to do is I want to next [7:56] maybe implement partition at and what I [7:59] want is some feedback on whether you [8:01] know as I go through that process if I'm [8:03] sort of doing something that makes sense [8:05] if the the you know I have some data [8:07] here is it actually being partitioned [8:08] the way I want. So what you can do in [8:11] Hazel is you can uh put what's called a [8:13] probe on any expression in the program. [8:15] Um there's a keyboard shortcut for that [8:18] uh command E or you can use a right [8:22] click menu. Okay. Um so far partition [8:25] out's not defined and so the feedback [8:26] that you get here right on screen is [8:28] that well partition out was is trying to [8:30] be called with the inputs three and then [8:32] the the rest of this list. So so far all [8:34] we're seeing is that pattern matching [8:36] works correctly, right? It's building up [8:38] the head element of that first example. [8:40] And you can also see the second example, [8:42] right? There's two tests down there. So [8:44] you can see the other call as well. You [8:45] can kind of toggle between the two. [8:48] Okay. [8:49] So now I'm going to go up here and I'm [8:52] going to define partition at um you can [8:55] see now the editing experience of Hazel. [8:58] How many of you have written a line of [8:59] code in the last month [laughter] [9:02] >> manually? Manually [clears throat] [9:05] I'm impressed. That's a lot. [9:06] >> [laughter] [9:07] >> All right. So, um, so I'm going to [9:09] define partition at. It's going to take [9:11] a a pivot element and a list and just [9:15] kind of leave leave some of these [9:17] syntactic obligations. So, so you know, [9:19] as you type, it's it's kind of doing [9:21] error correction and it's showing you [9:24] materialized feedback about that uh uh [9:27] the the the syntactic completions that [9:29] it's generating. Okay. So, if I go up [9:31] here, I'm going to define partition at. [9:34] I'm going to do it by case analysis on [9:36] X's. [9:37] If I want to partition the empty list, [9:40] I'm going to get two partitions that are [9:42] both empty. And then in the headcon's [9:44] tail case, I have to think about what I [9:47] want to do. So I know I'm going to [9:51] um recurse. [9:53] I want maybe the smaller and bigger [9:56] elements by recursing on uh the tail [10:00] with the same pivot. [10:05] Um, [10:07] what did I do wrong here? [10:14] >> Oh, partition at. Yeah, partition's in [10:16] our standard library for something else. [10:18] Okay. Um, thanks. All right. So, [10:22] partition [10:24] uh xtail. And now I know I need to do [10:27] something to compare the pivot element [10:31] against the heads. So maybe I'll do [10:33] something like this. And then I need to [10:35] figure out where to put things. So I can [10:37] kind of just uh try some things. If I'm [10:39] a student, this is a pretty typical [10:41] mistake that people make. They'll say, [10:42] "Okay, if x is less than head, it should [10:44] go on the smaller side. [10:47] Otherwise, it should go on the bigger [10:50] side." [10:52] So there's no type error in partition, [10:54] but this isn't correct. And if I go look [10:57] down here at the call to partition at, [10:59] what do you see? [11:01] Oops. All threes. [11:04] Ah, whoops. I put the I put the pivot at [11:08] every location rather than the actual [11:10] head element that I wanted. So if I go [11:13] here and fix that problem, I immediately [11:16] see, okay, I fixed that problem. These [11:18] are the actual elements from the input, [11:20] right? And this program is not complete. [11:22] it would be a parse error in a [11:24] conventional programming language. So, [11:25] we've moved it past parse error, past [11:28] type errors, all the way into runtime [11:31] feedback while we're editing. But [11:34] there's still a problem here, right? [11:36] What's the problem now? It's also not a [11:37] typing problem. [11:40] Anyone see the problem? [11:42] Wrong order. Yeah, I said the left side [11:44] is smaller and the right side is bigger, [11:46] but in fact, the smaller elements seem [11:48] to be on the right and the bigger [11:49] elements on the left. So that kind of [11:51] feedback allows me to think about that [11:52] with concrete data in a way that just [11:54] like staring at all these symbols you [11:56] would kind of like maybe miss that and [11:58] then end up with a reverse sorted list [11:59] perhaps at the end. And so I can [12:02] immediately I can I can come up with a [12:03] way to fix that. Maybe I should change [12:04] this comparison from less than to [12:07] greater than and I made that one [12:09] character edit and immediately the [12:10] feedback [clears throat] has changed and [12:12] I see that I've now gotten my partitions [12:14] correct. [12:15] Okay, [12:17] so that's the idea here is um live [12:20] feedback that's kind of actionable and [12:22] as immediate as one can compute it. [12:26] Okay, so I'm happy to actually stop and [12:28] try anything if people are curious. [12:31] Anyone want me to try something? Yeah. [12:39] >> Yeah. Yeah. Yeah. I mean you can't right [12:42] >> like do you get like blocked when [12:44] writing any code like how does [12:47] >> uh you don't get blocked from writing [12:49] code um the uh the way we're yeah that's [12:52] a system that probably could be improved [12:54] the we're trying to localize uh top [12:57] level kind of function calls that that [12:59] uh that hit a um recursion limit and [13:02] leave a hole there to say that like that [13:05] sub expression couldn't be computed [13:07] within the recursion limit but then it [13:08] can continue past that into other [13:10] computations. [13:12] Uh I won't attempt that at the moment. [13:14] But yeah, other questions. [13:20] Oh yeah, I can throw this at people if [13:22] they have questions. [13:28] [laughter] [13:29] >> Ouch. [13:34] >> What about side effects in programs? [13:37] >> Yeah, good question. So, Hazel is is [13:40] pure in the sense that it's you can't uh [13:42] you can't just throw in side effects [13:44] like network calls and file IO uh [13:47] directly in your program. I think that's [13:50] actually quite critical to this style of [13:52] live programming where it's really [13:53] updating you on every edit. You need [13:55] some way of controlling side effects. uh [13:58] if you had a program that was I don't [14:00] know making a trade uh you wouldn't want [14:03] it to make that trade on every key press [14:06] and then see what happens to your bank [14:08] account. Um and so you know I think [14:13] probably Hazel's more inspired on the [14:15] side effect side by Haskell uh where you [14:17] know you could do monatic IO and then it [14:19] would just compute the monad the IO [14:21] value and then you could hit run on that [14:23] when you actually want to run the side [14:25] effects that were computed in the pure [14:27] phase. Yeah. Okay. [14:31] back there. [14:34] >> If um a function's called multiple times [14:37] by a test case or is called recursively, [14:40] like how does that render in the like [14:42] example [14:42] >> in building here? Here it was Q sort was [14:45] already called twice by the two tests [14:46] there at the bottom. And so it actually [14:49] shows you both uh you can like scroll [14:52] between the two values. You can double [14:54] click to see them side by side. It kind [14:56] of defaults to kind of a collapsed view. [14:58] So the the test keyword isn't special in [15:01] creating those two cases. [15:03] >> No, the test keyword is just reporting [15:06] the result of the test in with this [15:08] little icon here live. Uh it's a [15:10] question mark now because we haven't [15:11] finished writing the function. It [15:13] results in a halt. But it could just be [15:15] any call to quicksort anywhere. Yeah. Um [15:18] if these values get too big, by the way, [15:20] that's also an important question to [15:22] address. You can click this drawer thing [15:24] and then the the it kind of takes up as [15:27] much space as it needs to show the value [15:29] and you have this like shift drag that [15:32] allows you to take up more or less [15:34] space. [15:37] Okay, [15:40] cool. Um so, yep. [15:42] >> Is there a way to control I guess what [15:44] version you want to see it step by step? [15:47] >> Yeah. Um so what you can do is if you um [15:51] let's see if you want to like trace this [15:53] call the values from like this so when [15:57] this was computed what were the values [15:58] of the intermediate variables in here [16:01] what you can actually do is right click [16:02] on this and do this step into [16:05] and what that does is it's in multiv- [16:08] view mode but okay when it's in single [16:10] sample mode it will uh take you to the [16:13] definition of that call and also um [16:17] select all the downstream samples in the [16:19] call stack from that uh the parent call [16:23] that's now pinned. And um that way you [16:26] can do this sort of like [16:29] debugger style kind of investigation of [16:31] particular places in the call stack [16:33] essentially. And so if you're interested [16:35] in a particular point in recursion in [16:37] the recursion, you would find the value [16:38] that produced that the you know the [16:41] recurs the the value you're interested [16:42] in and then pin that one and then you [16:44] would be filtered out to things that [16:46] were kind of in the same call frame. [16:49] Yeah. Does someone want to ask? Yeah, I [16:52] just pass it to you can go across. Yeah. [16:56] >> So I think there's a hint here. So maybe [16:59] this is like a first question, but like [17:03] do you have like can you put the holes [17:04] like anywhere? Like can you put like [17:06] replace one of the HDs with like a hole [17:08] and then [17:09] >> it's going to show up in the result like [17:11] do you have like partially known values [17:13] or [17:14] >> Yeah. [snorts] [17:14] >> Oh, I meant like in the when you push [17:15] things to the list, but this is also a [17:17] thing I guess like HD colon s like [17:21] instead of the HD you put like oh [17:24] >> yeah. [17:24] >> Oh yeah, cool. [17:26] >> Yeah. So it's essentially symbolically [17:27] evaluating the holes. It's passing. It [17:29] doesn't stop at a hole. It's not like a [17:31] it rays unimplemented. It's a it's a a a [17:35] term that passes through until it gets [17:37] sort of stuck in some elimination [17:39] position where it can't branch. Yeah. [17:42] >> Cool. [17:45] [clears throat] [17:46] Uh since I assume holes are first class [17:49] in Hazel, um [17:51] >> what are their exact type semantics? cuz [17:54] I assume if you have too many holes then [17:56] the types are just impossible to infer. [17:58] >> But surely in some situations they're [18:00] not as detrimental where you can infer [18:03] stuff [18:04] >> uh after you've even written a hole. So [18:06] like how does Hazel choose to solve this [18:09] problem? [18:10] >> Yeah, good question. Um so Hazel is [18:12] gradually typed meaning you can have [18:15] unknowns in the types as well. You can I [18:17] mean you can actually you know put a [18:19] unknown physically as a whole in in this [18:21] type like a list of unknown is the [18:23] return type of quicksort. Um so that [18:27] accounts for situations where there's no [18:30] known type because maybe you haven't [18:31] written something yet, right? Um that [18:34] also accounts for situations where [18:36] there's inconsistencies between [18:37] different places in the program. Like [18:40] different branches of a conditional [18:41] might have different types. So what does [18:42] what type does the conditional have? It [18:44] has an unknown type. Um we have a system [18:46] in a different branch that does type [18:49] hole inference what we call it. So it [18:51] does kind of a unification style type [18:53] inference to fill holes type holes in [18:57] the program on a [clears throat] on a [18:59] best effort basis and if it can't solve [19:01] the unification constraints. It gives [19:03] you kind of partial solutions to say [19:04] some of the constraints imply this. If [19:06] you fill it in with that then it kind of [19:08] does the error localization elsewhere [19:10] based on that uh that that choice that [19:12] you made. Um, so it's kind of live live [19:16] type [snorts] inference in that way as [19:17] well. [19:22] >> Um, so the whole trick seems pretty [19:24] important. Um, are there other notable [19:26] things that go into like the ability to [19:28] create this uh kind of inline debugging [19:30] experience? [19:31] >> Other tricks that go into creating this? [19:33] Yeah. [19:34] >> Yeah. I mean, um, yeah, quite tricky. [19:36] We're we're still actually working on [19:38] this, but um the yeah, the stuff I just [19:41] showed you with the pinning and keeping [19:42] track of call stacks and and and all [19:44] that stuff, you have to have you know an [19:46] uh an interpreter that has a lot of kind [19:48] of introspection and logging and stuff [19:50] in it. Uh and doing that efficiently has [19:53] been a bit tricky. Uh we are able to do [19:57] you know reasonably sized programs but [19:59] huge programs the data that's collected [20:01] would be too large. you can impose [20:03] sample size limits where you say don't [20:04] collect more than 10 samples at a [20:05] certain point that kind of thing. Um [20:08] yeah, but the engineering there uh my my [20:10] kind of um working model here is that [20:13] the way this would work in practice is [20:15] you you know when you're developing um a [20:18] function like quicksort or some analysis [20:20] that you're doing um you know you're [20:22] going to be working with smaller samples [20:23] of of of the data that's of the right [20:25] shape but not as many records, that kind [20:27] of thing. And so you would use the sort [20:29] of the version of the interpreter that's [20:31] instrumented [20:32] to support this kind of thing. Then and [20:35] then when you're done or if the function [20:37] sees a large input, it's jitted out to [20:39] something that has that doesn't have [20:42] that support but that runs more [20:44] efficiently. Uh we haven't built that [20:46] bit yet, but maybe we that should be [20:48] that could be oxel for example. Yeah, [20:51] this is implemented in in okamel. [21:01] Uh I'm a little curious about uh like [21:05] you know like the green [21:07] >> things like there are some [21:11] green things that aren't in cases that [21:14] are actually run [21:15] >> like so like if you input like the empty [21:18] list [21:18] >> yeah the light green [21:19] >> what do you see? [21:20] >> Yeah the light green I mean that is hit [21:22] and but not in this exact call frame [21:24] it's downstream of that call frame when [21:26] it hits the base case. Oh, okay. So, [21:28] like if like like if you input the empty [21:31] list, none of the other cases would be [21:33] hit. So, it just [21:34] >> Oh, if you just had the empty list. [21:35] Yeah, we can try that. [21:39] Um, [21:44] >> you might need one element just to just [21:47] to reach the function. [21:48] >> Yeah. I mean, it's just saying there's [21:49] no samples at any of those places [21:51] because it immediately hits that. [21:56] Oh, [21:56] >> okay. [21:58] Yeah. Okay. [22:00] >> Yeah, there's no samples in the in that [22:03] case. [22:07] Pass [clears throat] it over there. [22:08] >> Okay. Maybe one or two more questions. [22:10] >> Yeah. [22:12] >> If I have the same function that's [22:14] called multiple times, like for [22:16] instance, partition at because it's [22:18] recursing. [22:19] >> Yeah. Um, is the relationship between [22:21] call frames clear or am I going to just [22:23] see like [22:24] >> this thing collected tons and tons of [22:26] samples and the parent child [22:28] relationship isn't super obvious. [22:31] >> Um, yeah, that's a good question. So, we [22:33] have some experiments that uh we've been [22:34] doing. This is my Okay, [22:39] [laughter] [22:40] >> you should report it. [22:41] >> I think I think that was our uncomment [22:44] feature doesn't work [laughter] very [22:45] well at the moment. Okay. [22:50] Um, so if you pull up this little [22:53] sidebar, which we call the probarium, [22:56] um, it gives you some some quick [22:57] references and things, but it also has [22:59] this this color scheme that you can [23:01] select if you want, where instead of [23:03] everything being green, you have like uh [23:06] green, blue, and red. And that's [23:09] supposed to tell you sort of like things [23:11] are either above or below you in the in [23:14] the call stack. So in this case, the the [23:16] blue shows you that it's not this call [23:18] for anywhere. You got that data that's [23:19] like somewhere below. [23:21] >> Is there a way for me to like step into [23:23] the second level call so I can see some [23:26] red? [23:28] >> Yeah. Um to the second level call. Yeah. [23:31] So you know in the recursive call you [23:32] can say okay I want the next one. You [23:36] can also do steps which is like based on [23:38] a time a step counter like literal time. [23:41] Um, [23:42] so let me see if I can do a demo off the [23:44] top of my head here. [23:48] Okay. So, if you want the call where I [23:52] don't know, partition. [23:54] What am I trying to do here? Maybe some [23:56] of these. Oh, I think what's happening [23:58] is there's still a hole here. [24:02] There we go. [24:04] So you can do what I showed you before [24:06] of sort of like stepping into that and [24:10] then it's going to have pinned that [24:12] particular call. You can see the call [24:13] stack is up here. So it's like in two [24:15] levels deep of partition at Yeah. Yeah. [24:19] We're still working on some of the like [24:21] with recursion you just end up with a [24:22] lot of data and like UIs to concisely [24:25] show it on screen next to the code is [24:28] kind of an open question. Yeah. [24:29] [clears throat] [24:30] >> Okay. So I'll is it a quick question? [24:33] Okay, I'm I'm I just want to make sure [24:35] time is okay here. So, yeah, I'm gonna [24:37] continue here. Um, we've been working on [24:40] some improvements to the UI. Um, in [24:41] particular, you can do things like uh um [24:44] [clears throat] [24:46] wait, sorry. [24:48] So, let's finish writing quicksort here. [24:50] So, um we've been updating this little [24:52] backpack UI in order to show things in a [24:54] kind of a more concise way. Um, [24:59] if we want to call, if we want to finish [25:00] quicksort, we have to recursively call [25:02] quicksort on smaller and bigger. [25:08] And if I decide I wanted to do things in [25:10] the other order, you can you can swap [25:18] swap it back little animations. [25:22] And then we can finish it off with [25:27] that. And you can see, you might not [25:29] have seen, but the little the question [25:31] marks now became check mark here. This [25:33] test passed. This test failed because I [25:35] actually wrote the test wrong. Right? [25:38] That should be 7 910, not 9710. As soon [25:41] as I fix that problem, get a check mark [25:43] immediately. Right? So this whole cycle [25:46] of like doing a doing a bunch of code [25:48] writing and then like going through a [25:50] compiler waiting a few minutes for it to [25:52] recompile and then run the program and [25:54] then getting some error on a separate [25:55] terminal and trying to trace that back. [25:57] Like that whole dance I think is kind of [25:58] archaic and I think this is kind of a [26:02] better design for our programming [26:04] experience where you know the need for [26:06] rapid feedback is is taken seriously. [26:09] Um, now a lot of the feedback I've been [26:11] showing you so far, the feedback the the [26:13] the values have just been like lists of [26:15] numbers and so they're just showing up [26:16] as lists of numbers. Um, but Hazel [26:20] actually supports um, graphical notation [26:23] as well. So let me show you some [26:25] examples of that. So if you go into our [26:28] documentation system, here's our system [26:30] for tables. So this is actual code. [26:34] Okay, so you can write a table as a list [26:37] of tupils in in Hazel, but you can also [26:40] display it as a table, right? An actual [26:43] table that's laid out in a tabular form. [26:46] Um, and you can actually go uh go into [26:51] some some table that's being shown in a [26:54] probe and view that as a table as well. [26:57] This little popup here. And we have some [26:59] direct manipulation affordances as well. [27:01] So, for example, if I wanted to sort [27:03] this little table by score in a [27:05] different order, I can click this little [27:07] menu here, sort it by um in a descending [27:13] order. And now it actually inserted the [27:17] functional code to pipeline that table [27:19] into a sort function with the int [27:21] compare etc that you need there. [27:24] Okay, [27:26] so this isn't just for tables. you can [27:29] do uh uh we we have a system that we've [27:32] been developing for um kind of [27:34] customizable notation for whatever type [27:36] that you'd like. So uh we had a fun [27:39] experiment um on uh doing kind of a [27:43] algorithmic sound in Hazel. So you can [27:46] you can define a piece of music and do [27:49] some live coding. So you have a little [27:52] kick drum UI. This is just generating [27:54] some data underneath. You have a little [27:56] snare selector. have a a high hat, you [27:59] have some basic drums, you can produce [28:01] your melody using some uh musical [28:03] notation. You can actually just like [28:05] play the piano to to create a harmony, [28:08] and you can like compositionally put [28:09] that all together. Set your gains and [28:11] pans. This is literally just a number [28:12] underneath, but musicians love dials, [28:15] right? So, um this is this is a a [28:18] slider, but in a circle, basically. And [28:21] this is a pair of numbers drawn as a as [28:24] a little uh whatever those things are [28:26] called. and then just put it all [28:28] together. And then these probes can [28:30] actually not just show you values, but [28:32] play you values out loud. [music] [28:39] Okay, this is a little Macroish [28:44] project, so I'm not sure this is all [28:45] going to work, but I think it's more or [28:47] less. [28:55] Pause is not working on that one. [28:57] [laughter] [29:00] I guess this is just my life now. [29:02] [laughter] [29:07] Close that tab. Okay. [29:10] [laughter] Okay. So, you get the idea. [29:12] Yeah. [29:14] Cool. [laughter] [29:17] So, so that was Hazel. Um, if we all [29:19] were writing code manually, I think you [29:21] would be even more excited. But of [29:23] course what our lives look like today is [29:26] this. Um so um you know programming UIs [29:30] have have given way to these agentic AI [29:33] harnesses. Um so when I look at this you [29:36] know I uh I see uh a lot more feedback [29:41] loops right so we still have this sort [29:43] of human tool feedback loop. Um I also [29:46] drew the human human arrow because when [29:48] we collaborate we're giving feedback to [29:50] one another. But now we have this whole [29:52] kind of parallel track where there are [29:54] AI agents that are using their own set [29:56] of tools um which are kind of based on [29:59] but often slight variations of the tools [30:02] that we humans use to code um and uh [30:06] increasingly we are deploying agents in [30:08] what I called swarms in the abstract [30:10] right so there's multiple agents working [30:11] on a single codebase and uh they often [30:14] need to coordinate and interact with one [30:16] another uh within that codebase as well [30:18] and so um although this is kind of a [30:21] different world. I think a lot of the [30:23] same kind of design um thinking that [30:25] goes into designing good tools for [30:27] humans, taking into account the need for [30:29] feedback uh good, you know, timely and [30:32] um easy to to digest feedback is still [30:35] applicable in this world where there's [30:37] all there's just more feedback loops in [30:40] in in the system. Um and so timely and [30:43] quickly processed feedback is ideal for [30:44] all of the feedback loops in this [30:46] system. Um, and I think this is going to [30:49] be especially the case once we have uh [30:51] these promised thousand plus token per [30:53] second AI agents, right? If you use uh, [30:57] you know, current generation frontier [30:58] models, they're maybe, you know, less [30:59] than 100 tokens per second, but people [31:01] are are building these, you know, wafer [31:04] size A6 for for running um, uh, frontier [31:08] models. And if we have these thousand [31:10] token thousand plus token per second AIS [31:12] then uh we we could imagine a world in [31:15] which we're actually bottlenecked on the [31:17] other the tools themselves the feedback [31:19] that these agents are getting from um [31:22] the system on on the actions that [31:24] they're taking. And so I think this is [31:26] only going to become more important as [31:28] as the performance of these systems goes [31:30] up. I forgot to mute Slack dur before [31:33] the talk. [31:35] Um so let me talk about some of these [31:37] feedback loops. So the AI agent to its [31:40] tools um uh feedback loop I think has a [31:44] lot in common with the humans to [31:46] programming tools feedback loop u but [31:48] also some important differences. So I [31:51] think the feedback in agent loops is [31:52] also often delayed and costly to [31:54] process. Uh modern AI systems tend to [31:57] not make a ton of syntax errors that [31:59] kind of cross that out. They do [32:00] occasionally especially if you're giving [32:02] them kind of more obscure languages to [32:03] work with. Um but uh they're able to [32:06] actually write Hazel code perfectly well [32:08] even though there's no Hazel in the [32:09] training data. Um but things like type [32:12] errors uh still cause the sort of gaps [32:14] in the editor services. So if they want [32:16] to try you know make a make a a change [32:18] and then like run the code in the [32:20] agentic harness and see what happens if [32:22] there's a type error anywhere uh there's [32:24] no runtime feedback everywhere. Same [32:26] problem as for humans but now for agents [32:29] and agent swarms as well. This is a [32:31] problem. Um there's a new problem that [32:33] comes up which is that uh these things [32:35] are like goldfish, right? They forget [32:36] everything they've ever done every time [32:38] you start a new agent. And so there's [32:41] this additional sort of feedback loop [32:42] where they need to like get information [32:44] quickly to recontextualize themselves [32:46] every time you give them something new [32:48] to do. Uh and then they're uh still [32:51] using compilers. they're still executing [32:52] code and so the the recompilation [32:55] re-execution times are still important [32:58] and um uh processing large textual logs [33:01] is also costly uh when it's when you're [33:04] feeding them into AI systems. Um I'm [33:06] just realizing I forgot to show you one [33:08] quick thing in the demo. Let me actually [33:09] do that before we continue since I think [33:12] it's relevant. So let's go back to this [33:14] demo here. Um I'll turn off all the the [33:18] probes here. Turn this off. So um if I [33:21] write another test here um while we've [33:24] already written a couple of tests and [33:26] the code is kind of let me go to the [33:28] version where it's actually finished. [33:30] Sorry. [33:32] Um [33:33] scratch mode here. So this is with [33:36] regard to the feedback of the the [33:38] re-execution. Okay. So this is a [33:40] finished version of quicksort. I've [33:41] written a couple of tests. Um if I write [33:43] another test uh I shouldn't have to pay [33:46] the cost of re-executing these previous [33:48] two tests, right? [33:50] uh and if I want live feedback, this is [33:52] really a constant problem. I don't want [33:54] to like rerun the program from scratch [33:56] every time I type a new character. And [33:57] so we've been putting a lot of thought [33:59] into incrementality in the programming [34:00] system in a very fine grain way where [34:02] small edits should cause uh small deltas [34:05] in the the recomputation of both type [34:07] static information types and dynamic [34:09] information. And so I'll show you how we [34:11] do that in in part in Hazel for um [34:14] execution. And I can do that by turning [34:17] on [34:18] um so this is happening anyway, but I'll [34:21] turn on the visualization for it. So you [34:22] can see these little uh blue um nodes [34:26] are are nodes in the a that aren't [34:28] re-executed from the last edit. And so [34:31] if I type a new uh test here, [34:35] [clears throat] [34:40] you can see it's [34:46] It's uh saving all of the previous calls [34:49] from all the previous tests. And even [34:50] like partway through entering this line, [34:53] it noticed that like it already had [34:55] called the lefth hand side of the [34:57] equality. And so it didn't need to [34:58] re-execute that. It was just [35:00] re-executing the equality test as I [35:03] edited the right hand side of the [35:04] equality. Okay. Okay, so that's doing a [35:07] basic kind of a a data flow analysis uh [35:10] of of this code and and um and caching [35:14] the previous values. Um in in more uh [35:17] recent work, we've been thinking about [35:19] the problem of like what if you go in [35:20] and edit the functions themselves in [35:22] small ways like I did the change earlier [35:24] where I changed x greater than head to x [35:26] less than head. There's still a bunch of [35:27] computations that maybe could have been [35:29] saved from before. And so we've we have [35:31] a paper coming out uh at LA 20 to 26 [35:35] later this year on what we call um [35:37] shortcut memoization which is um a [35:40] system that that saves intermediate [35:42] computations as well in a in a memo [35:44] table that that is abstracted over by um [35:47] by pattern variables. And so you can say [35:50] every time I see you know a length call [35:52] on a list of the form you know a con b c [35:56] con nil it's going to return four. So [35:59] let me just save that pattern and then [36:02] we have some very efficient data [36:03] structures and algorithms for uh looking [36:06] things up in this patternbased memo [36:08] table. So we've been putting a lot of [36:10] energy into incrementality both on the [36:12] execution side and the type checking is [36:14] also incremental. you have with [36:15] semantics for incrementally recomput not [36:18] not just producing the or checking the [36:20] type but actually producing all the [36:21] intermediate type information that you [36:23] need for showing stuff like at the [36:25] bottom of the screen there like the [36:26] types of intermediate results. So we had [36:30] a paper last year on the semantics of [36:31] that and we proved it correct. So it's [36:34] basically a much more fine you know [36:35] build systems kind of do this kind of [36:37] incrementality at the the level of a [36:38] compilation unit. We've been thinking [36:40] about this at the level of individual [36:42] expressions within a programming [36:43] language. And we think that as you make [36:45] uh fine- grained edits in a live [36:47] programming setting or as lots of agents [36:49] make lots of edits that like doing that [36:50] in a very fine grain way kind of reusing [36:52] as much as you can is really important. [36:56] All right, [37:01] cool. Let's continue. [37:04] Um so in in terms of um this AI agent [37:07] tool loop, I think the way to think [37:08] about it is that we need to build good [37:10] live incremental idees for AI agents [37:13] just as much with the sort of the same [37:15] design um thinking that we put into uh [37:20] tools for human programmers. Uh we need [37:23] incremental compilation, incremental [37:24] execution. We need to think about this [37:27] sort of gaps in editor services and we [37:29] want to give so so we have an AI [37:31] assistant. I don't have time to give a [37:32] full demo of the Hazel AI assistant. The [37:34] Hazel AI assistant works kind of like [37:36] you know your your cloud code kind of [37:38] harness except the actions that it [37:40] performs and the information that it has [37:43] uh available to it to to perform those [37:45] actions is entirely based on this [37:47] semantic model. This kind of like model [37:49] of type functional programs with live [37:51] execution data and holes for incomplete [37:54] pieces and errors. Uh so it can do [37:57] things like it's not operating as a a a [38:00] layer on top of the bash shell. It's [38:01] operating as a layer on top of the [38:03] structured action language of Hazel. And [38:05] that allows it to do uh uh semantic [38:08] search. Um it allows it to do semantic [38:11] contextualization to find like the [38:13] actual definition of this thing even if [38:14] it's far away, even if there's multiple [38:16] other functions with the same name, that [38:18] kind of thing. [38:20] um and uh to rely on this fine grain [38:22] incrementality and even use that kind of [38:24] inline feedback with live data that I [38:26] showed you in Hazel, right? The little [38:28] the on on by the side of each line you [38:30] have live values. You can textualize [38:33] that, put it into an AI agent as it [38:35] writes code and it can kind of get more [38:37] rapid feedback to see if it wrote that [38:39] function correctly, if the data that's [38:40] flowing through it is what it expected. [38:42] Um and so we've started to do some [38:43] experiments with frontier models and and [38:45] kind of midscale models as well on um [38:49] making use of that information. Um short [38:51] short uh summary of ongoing work is that [38:54] it works. These agents can use these [38:56] kind of structured action languages. [38:58] Even though they're trained on bash, [38:59] they can use these these richer [39:01] structured action languages and they [39:03] actually um I think they they sort of [39:05] like that inline feedback because [39:07] they're very they're trained to check [39:09] their work aggressively. Um, and if they [39:12] can do that as they go, they have less [39:13] of a kind of burden at the end of the [39:16] whole process the same way that humans [39:18] like to check their work as they go. Um, [39:20] so we're we're turning this into form, [39:22] you know, more formal studies and [39:24] results and things like that. But, uh, [39:25] just uh, intuitively, it seems to to [39:27] work nicely. And it also seems to [39:29] decrease a little bit the um the token [39:32] usage of these models because uh they're [39:35] they're doing kind of more uh surgical [39:38] edits rather than rewriting an entire [39:41] function um because they have richer [39:43] structured editing available. [39:47] Okay. And then I also want to talk about [39:49] this feedback loop, the humans and AI [39:50] agents loop. So I think the the feedback [39:52] between humans and AI is that's sort of [39:54] the like you know the AI does some stuff [39:56] and then you type some stuff to it and [39:58] uh it tells you some stuff right so that [40:00] that can often that's often bottlenecked [40:02] on humans right I I don't know about you [40:04] but I I have you know maybe 50 open PRs [40:08] in my various projects that I need to [40:10] review [40:12] because AI has just accelerated [40:14] everyone's you know velocity with with [40:16] PRs. Um, and so if we can do things to [40:19] make that easier, I think we can uh we [40:21] can accelerate the the overall process. [40:24] And so we've been working on a project [40:25] with Hannah Potter at the University of [40:27] Washington where we're bu building [40:29] what's called a narrativized change tour [40:31] system. Uh this is not in Hazel. This is [40:33] initially for GitHub PRs. So um the idea [40:36] is basically you just have uh all of the [40:38] the hunks in in your GitHub pull [40:40] request. All the have to kind of form a [40:42] narrative. You create a narrative with [40:44] the hunks inside of it. It's basically a [40:45] fancy markdown file with an exhaust [40:47] checker that checks that you've [40:48] described everything and um and then [40:51] some cloud skills and and so on to [40:53] create initials versions of these and [40:55] narrativizing a pull request in this way [40:58] where you describe the code in an order [40:59] that makes sense I think is a really [41:01] critical thing um rather than our our [41:04] kind of usual way of approaching this. [41:06] Had a lot of great conversations with [41:08] some Jane Streeters earlier today about [41:09] this. We have this available as a as a [41:12] VS Code plugin if anyone wants to try [41:14] it. We're studying some aspects of this. [41:18] [clears throat] [41:19] And then finally, I think AI agents as [41:21] you get more and more of them [41:22] collaborating on a codebase, you sort of [41:24] start to hit the limits of standard [41:26] version control systems. It's not often [41:28] not built for thousands of agents [41:29] editing a codebase simultaneously. [41:32] Um, you know, questions like who else is [41:34] editing editing this right now are [41:36] difficult to answer with like uh with [41:37] Git at least. Um, and uh I think that's [41:42] an important question for AI agents to [41:44] to sort of understand otherwise they end [41:45] up in this sort of like loop of uh [41:49] editing the same thing and then [41:50] resolving conflicts in a conflicting way [41:53] and then having to resolve the conflicts [41:55] between the conflict resolutions and uh [41:59] you can actually get into like you know [42:02] spending 50k in tokens trying to to [42:04] build something because of that. Um [42:06] there was a really interesting project I [42:08] saw where they tried to build a verified [42:10] compiler from JavaScript to to web [42:12] assembly and without a ton of [42:14] coordination between the AI agents. They [42:16] all just picked the lowest hanging fruit [42:18] all the time. They all kind of [42:19] conflicted with one another uh in minor, [42:22] you know, stylistic ways and you ended [42:25] up spending a lot of tokens with not a [42:27] lot of output. So I think improving the [42:29] the collaboration story is something [42:30] we're really interested in. Um so we've [42:33] been working on a variety of new [42:35] foundations for collaborative editing as [42:37] well at at PPP. Um last year we [42:40] developed this system for collaborative [42:42] tree editing rather than collaborative [42:44] text editing which is what our current [42:45] systems are based on if these things are [42:47] using structured edit actions. We should [42:48] have a system where um there's there's a [42:51] commutativity property between the the [42:53] structured editing actions on trees. And [42:55] we developed such a thing and and did [42:56] various proofs. I want to explain what's [42:58] going on here, but essentially if you [43:00] are familiar with a CRDT, it's a CRD a [43:02] graph CRDT for trees. The reason for [43:05] that is we made code relocation a first [43:07] C class primitive in this system which [43:10] solves a lot of weird conflicts. I'm [43:12] sure you all have encountered this where [43:13] if I move a one move a function here and [43:15] you move it there and someone makes an [43:17] edit to that one, you just get [43:19] duplicated versions of the function and [43:20] no conflict when there should be a [43:22] conflict. So we we address all those [43:24] problems in the system and we think this [43:25] is a really solid foundation for um [43:28] structured editing of of tree data [43:30] structures. I won't say too much there. [43:33] Um we're also combining this with some [43:34] work that the folks at the Unison [43:36] project have been doing. Um how many of [43:38] you have heard of Unison? [43:41] You okay so Unice is a really [43:42] interesting story for version control of [43:44] code in particular where um code is [43:47] never deleted from your um repository. [43:49] you only ever get new versions of the [43:51] code and variable references are by hash [43:53] by content address hash rather than uh [43:56] by name and so you have to do an [43:58] explicit refactor to like move you if [44:00] you if you define a new version of I [44:02] don't know list.m mapap I don't know [44:04] that's probably a bad idea but uh if you [44:06] do that then you don't break all the [44:08] existing code you just get two versions [44:09] of list mapap and and you can update uh [44:11] the ones that you want to update and not [44:12] the ones that you don't um and and this [44:15] works really well for uh AI agents in [44:17] particular where they're they're [44:18] creating all sorts of different versions [44:20] of these things. They can um they could [44:22] sort of work in parallel and then do a [44:25] resolution pass or a refactoring pass [44:27] later for cleanup instead of um dealing [44:30] with constant refactorings across a code [44:32] base. We're combining that with the [44:34] growth stuff that I just showed you. [44:35] Then finally, I want to talk a little [44:36] bit about trustworthiness, right? So, if [44:38] you have these AI agents, I'm not going [44:40] to explain the whole diagram here either [44:42] yet, but um if you have a bunch of AI [44:44] agents interacting in in an environment, [44:46] some sort of secure execution [44:47] environment where they're sensitive [44:48] data, sensitive effects that you can [44:50] perform, you don't want them to just [44:52] have like root access to your terminal. [44:55] Um I don't know about you, but I turn on [44:57] unsafe what is what is it called? [44:59] Dangerously skip permissions maybe way [45:01] too often on on cloud code. Um I think [45:05] that's a really bad idea. And uh there's [45:07] this there's this long Yeah. [snorts] [45:10] [laughter] [45:11] Tautology. Yeah. Uh [45:14] dangerously skip permissions. I wonder [45:16] if that's dangerous. Um anyway, so [45:20] object capabilities, if you if you [45:22] haven't heard of this idea, it's it's an [45:23] old idea from software architecture [45:25] where you sort of control which [45:27] capabilities are available in a fine [45:29] grained way by defining little object [45:31] APIs. Um so you know your root component [45:35] has like the IO file IO capability but [45:38] then you can create an attenuation of [45:40] that for logging where you can only do [45:42] appends to a single log file and if you [45:45] pass that to a component all it can do [45:46] is log it can't do general IO and so if [45:49] you have a language in which you can't [45:50] sort of forge capabilities which is [45:52] really critical there you you get a much [45:54] more kind of um reasonable able to be [45:58] reasoned about system in terms of where [45:59] the where the effects could be happening [46:02] and so I I think that is uh how we [46:03] should design the tool languages that [46:05] agents use. Um we should use an object [46:09] capability system so that that we can [46:11] define baseline provably correct [46:13] policies for what kinds of effects these [46:15] things can have and then attenuate them [46:17] on a per task basis either manually or [46:20] with the assistance of a um supervisor [46:24] agent of some sort. And so there's a a [46:27] workshop paper at Hope that goes into [46:29] the architecture of this and talks about [46:30] how we could actually use proof [46:32] assistance to to uh prove the [46:34] correctness of our our baseline [46:35] policies. Uh we've been doing some work [46:37] with um medical privacy people here. So [46:40] doing things like using information flow [46:42] control in the design of the the the [46:44] tool language um to to be able to prove [46:47] things like information from a patient's [46:49] email only ever ends up in their own [46:50] chart and not in anyone else's chart or [46:52] anyone else's email. Um, and I think [46:55] that's a really critical thing to be [46:57] able to use these in in sensitive [46:58] environments. Um, [47:02] cool. So, let me conclude here with kind [47:05] of a vision for what all of this [47:06] together could look like. So what I'm [47:09] imagining in the future is that instead [47:11] of um instead of everyone having a bunch [47:14] of different repositories that uh that [47:17] um that interact [clears throat] [47:20] that that sort of l are storage for code [47:23] what I'm imagining is instead we have a [47:24] big network of live programs live [47:28] executing programs. [47:30] This needs to be built in a way that [47:32] supports um both human and AI use in a [47:36] collaborative way. So that's where our [47:38] work on new foundations for [47:39] collaborative editing I think is is [47:41] really important there. And it needs to [47:43] be built in a way where if I make an [47:44] edit that causes a a syntax error or a [47:47] type error, it doesn't bring down the [47:48] entire commons, right? So like like a [47:51] Wikipedia, right? If someone made a [47:53] syntax error on one page of Wikipedia [47:54] and the whole thing went down, that [47:56] can't happen, right? So we need that [47:59] that capability there. We need human the [48:02] human role especially sort of [48:04] non-programmers I think is a really [48:06] important category here. Our role has to [48:08] be somehow to like monitor what's going [48:10] on in terms of these kind of reports and [48:12] things like that where there's computed [48:16] elements like this graph that you can [48:18] expand and and sort of manipulate as you [48:21] see fit and maybe even manipulate in [48:23] sort of these direct ways where the the [48:25] agent that wrote this code leaves a [48:26] slider for you because it doesn't know [48:28] exactly how how wide the bar chart [48:30] should be, right? And so that's what the [48:32] live literal, the the sort of graphical [48:34] editing stuff that I showed you allows [48:36] you to do, like I showed you with the [48:37] music, for example. And so imagine [48:39] something like Wikipedia where the whole [48:42] system is a live program being edited by [48:45] thousands of humans and AIs that's [48:47] producing these kinds of like hybrid [48:49] symbolic and graphical um pages where [48:52] each page is a module in the O'Camel [48:54] sense and um where edits are [48:58] incrementally recomputing exactly what [49:01] is needing to be recomputed. Um, I think [49:05] that is the kind of environment in which [49:07] we can kind of imagine a future of work [49:09] where like lots of humans and agents are [49:11] are being productive together. Um, and I [49:13] think it also brings up a lot of fun [49:16] computer science problems that I've been [49:18] thinking about, but I think there's lots [49:19] more to solve. I'm excited to to think [49:22] about this and this is from a climate [49:24] science um workshop that uh uh that I [49:27] put together, broming for the planet. So [49:29] I'm excited to think about this. I'm [49:31] going on sobbatical at Cambridge for a [49:32] year to work with climate scientists um [49:35] on building this kind of system for [49:37] large scale climate modeling where all [49:38] these different systems need to actually [49:40] talk to another. The fish modelers need [49:41] the ocean temperature modelers, they [49:43] need the the um the ice sheet modelers [49:45] and so on, right? So, um building these [49:48] kind of world models that are live [49:49] programs, not just databases, I think is [49:52] is a really uh exciting uh future for [49:55] computing. Um, and so hopefully you can [49:58] see at least the hints of how some of [50:00] what I've been working on in in our [50:02] group have allows us to think about [50:05] this. So I will stop there and happy to [50:08] take more questions if there's time. [50:19] >> Yep. Does someone want to pass the [50:22] >> Yeah, you can start running. Uh so you [50:24] mentioned that you know we don't have a [50:26] good way of having thousands of agents [50:28] interacting on the same codebase and a [50:30] kind of editing model for that. [50:31] >> Yeah. [50:32] >> But like I kind of think we do like we [50:34] have one here. we have like a few [50:35] thousand agents who are like interacting [50:38] in a big codebase together and you know [50:41] there there's a model where you like you [50:42] know you make changes and you merge them [50:43] together and all of that and like and [50:44] sometimes there are conflicts and then [50:46] you have to rebase them and like but [50:48] like that kind of works and I'm kind of [50:50] like I [50:50] >> maybe I was too strong to say that [50:52] doesn't like it it sort of starts [50:54] creaking a little bit like I was talking [50:56] to some lean folks recently right and [50:58] that's that's a that's an example of a [51:00] computational comments the math lib [51:01] effort that the lean folks are doing [51:03] >> and a lot of them are like we need to [51:04] rebild build the you know the compilers [51:06] and things here because there's just the [51:09] agents are doing too much editing too [51:11] fast. Uh I think the collaboration side [51:13] with git is also a little bit um iffy [51:17] for them because they want to understand [51:19] if there's a bunch of other agents [51:20] proving lemas related to the thing [51:22] they're interested in. They want to like [51:24] know that before the lemmas are done and [51:27] committed. Do I think it's a more like [51:29] if it's a little bit more Google doc [51:31] style where you see the cursors going [51:32] around but there's still get style [51:34] infrastructure underneath I think that's [51:36] more what I have in mind not a like [51:37] throw it all away like we don't have any [51:40] idea how to do collaboration that's not [51:42] maybe that was coming across too strong [51:44] >> yeah I guess I wonder in some like I [51:46] think my mental model for a lot of this [51:48] has been that many of the affordances [51:50] that we've built for humans are are like [51:52] kind of the same affordances there and [51:54] like we do you know there's there are [51:56] ways of like you know you have will like [51:58] literally like they'll they'll write [51:59] features but they'll also use Google [52:01] Docs and they'll have ways of like [52:02] collaborating communicating about the [52:04] work that they're doing as way of [52:05] partitioning up the work. [52:07] >> Yeah. Yeah. [52:08] >> Like I'm kind of curious to what degree [52:10] does like the thing the kind of fine [52:12] grainedness [52:13] >> Yeah. [52:13] >> that you're kind of like the big change [52:15] here is really about like the [52:17] granularity and I'm kind of curious like [52:19] how that plays into [52:21] >> what you think happens at scale. [52:25] Um yeah, I mean I think it's important. [52:28] I don't think like you can't do [52:29] largecale work without that granularity. [52:32] Obviously that's not true. We do large [52:34] scale work. You all do large scale work [52:37] with without that granularity. Um I [52:40] think [52:42] it's it sort of becomes more important [52:44] the more large scale kind of rapid [52:47] iteration on the same components is [52:50] happening versus like if you've created [52:53] good architectural barriers and things [52:55] are happening in different components [52:57] but there's only one or two agents in a [52:58] single component at a time. I think then [53:00] the more traditional view still holds. [53:03] Um the other aspects of you know needing [53:05] new collaboration primitives I think are [53:07] still relevant as well. I think being [53:10] able to refer to old versions within a [53:12] single codebase and not having to settle [53:14] on a single canonical version when you [53:15] do the like the version resolution and [53:19] opam or whatever. I think that's an [53:20] important thing to get right and unison [53:22] has gotten a really solid foundation [53:24] going on that um you know handling code [53:27] relocations correctly rather than doing [53:29] what we do now in git is I think really [53:31] important. So yeah, those I think [53:34] they're all like little things that we [53:36] need to tweak, not like a throw it all [53:37] away there. Yeah, [53:43] I'll pass it over there. [53:47] >> Have you had a chance to apply this [53:48] large scale collaboration format to math [53:51] and formal ver formal proof of in math [53:54] yet? [53:55] >> Um, and we haven't done large scale [53:58] collaboration for anything yet. We're [54:00] working on foundational aspects there. [54:03] Um on the math side, I haven't I didn't [54:04] talk too much about our group's work [54:06] there just for the sake of time. Uh we [54:08] are adding um uh the improver [54:11] capabilities to Hazel. Uh we're actually [54:13] basing it on more of an Isabel style [54:15] design uh rather than a a lean [54:18] dependently type full spectrum dependent [54:20] types design. I can talk offline about [54:23] why I think that's an interesting design [54:25] space. Um I think obviously in a world [54:28] where you know the cost of proofs has [54:29] changed from you know it used to be you [54:32] needed super expert engineers to do it [54:34] and now you can ask Fable to do it. Um I [54:37] I I think it's really important that [54:39] there be kind of proofs throughout the [54:41] system. There be properties that uh [54:44] serve as a way for us to review what's [54:45] happening in kind of a more abstract way [54:48] like code review in terms of do the [54:49] invariants make sense and then oh [54:52] there's a proof that the invariant's [54:53] true and so collectively this makes [54:54] sense. I think that's really going to be [54:56] a nice future. And I also think just [54:58] math and science and and technology, [55:00] these things have used separate tools [55:02] for a long time. And it'd be nice if we [55:03] could like do everything in a common a [55:06] commons. [55:08] Yeah. [55:14] >> Um this is really cool. Um I have two [55:16] questions. So I think they kind of both [55:18] get at the idea of state. Um [55:21] >> like in this example I'm trying to think [55:23] about how we might apply this here like [55:26] where you have a bunch of notebooks and [55:28] they sort of all are operating over some [55:30] set of data sets like the data has to [55:32] live somewhere how do you imagine that [55:35] existing like even in this planet hazel [55:37] example. [55:37] >> Yeah. Yeah. Totally. Um [55:40] let's see. So you know notion like like [55:42] I like to think of this as kind of a the [55:44] same computational model as as a giant [55:47] spreadsheet right? So at least [55:50] notionally the data and the computation [55:51] in a spreadsheet both live in the [55:53] spreadsheet. Um for really large scale [55:57] like you know planetary scale data sets [56:00] that that's not literally what would [56:02] happen. It's not like literally sitting [56:03] in your in your memory of of the of your [56:06] IDE. Now we have this uh project called [56:09] our foreign data interface. Uh so it's [56:11] like a foreign function interface but [56:13] for foreign uh data sets um where the [56:16] runtime system has some like pluggable [56:18] components um inspired by if you're [56:20] familiar with Apache Apache Spark [56:22] project it has this push down API that [56:25] allows you to say like notionally I'm [56:27] doing a functional transformation on [56:29] this data set but actually it lives in [56:31] some SQL store somewhere on a remote [56:33] server and it's just going to like turn [56:35] all the the filters into SQL uh calls [56:37] and things like that. Um, so I think [56:40] we're gonna basically have a JIT to [56:42] spark [clears throat] for the sort of [56:44] really large data sets. Uh, but [56:46] definitely open to discussion there. I [56:48] know you all work with large data sets a [56:50] lot. So if you have thoughts, happy to [56:51] discuss further. [56:52] >> Cool. Thanks. [56:56] >> Uh, yeah, I think this really cool. Um [56:59] based on like Hazel and like this [57:00] graphic, I assume that you envision a [57:02] model of code or computation in general [57:05] more in terms of treebased rather than [57:08] everything projected down to like in an [57:09] order um just like text. Um so my [57:14] question is like this clearly has a lot [57:16] of vision behind it. So do you think [57:18] that um the best possible thing you can [57:22] develop is a guiding prescription on [57:26] code should be treebased and in Hazel [57:28] this counts as like incremental [57:30] annotations and things like that. [57:32] Whereas for this you have the ability to [57:35] um compartmentalize editing certain [57:38] graphics and things like that or do you [57:39] think that your goal for making the [57:41] foundation for the primitives is [57:43] actually engineering thing these things [57:45] to be used for other people or I guess [57:48] like what scope do you think you can [57:50] actually enforce this um opinionated [57:52] view on the future? [57:55] >> Uh yeah that's a good question. I mean, [57:57] so the treebased aspect of it, it's not [58:00] so much that I'm like a, you know, I I I [58:03] think everything's a tree. It's that I [58:06] think, um, type theory is a good basis [58:11] for ontologies. [58:13] Um, [58:15] a much better basis for ontologies than [58:17] like if you remember RDF in the sort of [58:21] semantic web. I don't know if everyone [58:23] remembers that, but [58:25] you're Don't look it up. [laughter] [58:30] You know that that models all knowledge [58:32] as a binary relations between untyped [58:35] things. Of course, there are relations [58:37] that are not binary. There are different [58:39] types of things in the world. So, I I [58:42] think if there's any sort of strong [58:43] opinion I have, it's just that like the [58:45] the computational common should be [58:47] rooted in having products, sums, and [58:50] functions and modules. Um, I think [58:54] that's probably not so controversial in [58:56] this room. Maybe your your your bigger [58:58] question about how how much control do I [59:00] have over the world? Uh, not much, [59:04] right? But I think I what I'd like to [59:06] tell, you know, new students that want [59:08] to work in the lab, you know, when they [59:09] think about having an impact with this [59:11] kind of work. Um, [59:14] my my vision of translational research [59:17] in in my group is translation by [59:19] jealousy. [59:21] All right. So we build something really [59:23] beautiful [59:25] and kind of correct in a way that has [59:27] like math proofs behind it and uh either [59:31] it gets enough engineering behind it at [59:34] some point that it works or like there's [59:36] enough jealousy about what we've built [59:38] that a bunch of people in other [59:40] communities go and build similar things. [59:43] Uh certainly I've seen a lot of that you [59:45] know in recent years it's certainly not [59:47] us uh exclusively driving it but people [59:49] are working a lot on this problem of [59:51] integrating graphics into code. Uh live [59:54] programming has had a lot of work going [59:55] into it programming with holes. A lot of [59:57] other programming languages have holes [59:59] in various forms. um you know if you [60:02] don't have purity you can't do the sort [60:04] of like live programming on every key [60:05] press but you can like you can do it on [60:08] a best faith basis right where you're [60:10] just like you accept that if there's [60:12] side effects here they're just going to [60:14] get run or you do a you know a semantic [60:17] analysis and only run it on on pure code [60:19] actually the Chrome dev tools do that [60:21] for JavaScript you can get [60:22] [clears throat] live execution on [60:24] JavaScript but it like does a very [60:26] shallow purity analysis to make sure [60:27] there's no effects happening [60:30] um conservative. Yeah. Anyway, so I [60:33] don't know if I answer your question, [60:34] but that's my ethos there. Yeah. [60:42] >> Hi. Um yeah, once again, great talk and [60:45] I I really like particularly the care [60:48] that's that put into the presentation. [60:50] Like making things be pretty h has so [60:53] much value that I think especially as [60:55] programmers sometimes we forget. [60:56] >> Yeah. A lot of credit to David and to [60:58] Andrew Glenn and other of mine. They are [61:01] very good [clears throat] designers. [61:02] >> Um my question for you is as [61:06] as we go into like what I'm seeing on [61:08] the screen here where you know we we [61:10] take the code and we make tables out of [61:12] it and we have graphics and they have [61:13] sliders and we go into some of the [61:15] things you talked about about swarms of [61:17] agents that might work on a commons and [61:20] you know modify their own little bit of [61:22] code. [61:22] >> Yeah. Uh I have kind of like a [61:25] philosophical question which is I [61:27] imagine that will require a lot of [61:29] change in [61:31] what we even think of as code like right [61:33] now we think of code as [61:35] >> ultimately it is [61:36] >> it is text on a file that gets compiled [61:39] but are we going to get further away [61:41] from that like how much will humans [61:43] understand what what all the turtles [61:46] that are underneath? [laughter] [61:49] >> Yeah. Um how much will humans understand [61:51] the turtles? I don't know how much we [61:54] need to keep building on the same [61:55] turtles is also unclear given that like [61:57] the costs of adopting and building new [62:00] things has changed dramatically. [62:03] um in particular adoption costs for new [62:05] languages, right? Like it used to be it [62:07] was like so difficult to get a large set [62:09] of libraries in your new language and [62:11] now I just you know I can build a [62:13] library for whatever I want in Hazel by [62:15] just like leaving cloud running [62:16] overnight, right? Um I can port code [62:20] from other languages very easily to [62:22] Hazel. We've done a lot of I mean [62:23] there's you know there's a lot of just [62:25] randomly ported things that we've used [62:27] for case studies for our data analysis [62:29] work. for example, it's taking Jupyter [62:31] notebooks and turning them into Hazel [62:32] notebooks. Um, so I [snorts] think the [62:35] cost structure has changed and I think [62:36] it's actually high time for us as a [62:39] community of computer scientists to [62:41] think about like [62:43] what should the future look like. It [62:46] like we have an opportunity here to [62:48] build the right things instead of [62:49] [clears throat] just like having to [62:51] confront network effects and the billion [62:54] dollars of software engineering effort [62:55] is needed to build a standard library [62:57] and blah blah blah, right? So like I [62:58] think this is a good time to be in this [63:01] space. I think we just have to be bold [63:04] enough. [63:12] >> So this dynamic environment that you're [63:15] describing where [63:17] >> things are constantly changing and [63:20] [clears throat] it's live and so people [63:21] are also interacting with it. It feels [63:23] like [63:24] >> we've kind of just entirely done away [63:27] with the distinction of like [63:30] >> what version of my code is in [63:32] development versus what's already been [63:34] deployed. And [63:35] >> how do you think about uh deployment? [63:38] What what does deployment mean in a [63:40] world like this? Or how do you [63:42] >> make sure that you're not just like [63:43] immediately breaking things for people? [63:46] >> Yeah, I'm a bit um of two minds here. [63:50] There's a part of me that's a bit uh [63:52] excited by the chaos of like everything [63:56] is live all the time. Um you know in a [64:00] in a climate science setting I think you [64:02] know we get new sensor data every [64:05] millisecond from millions of sensors all [64:08] over the world. We get new satellite [64:09] data for every 10 square meters of the [64:12] globe every single day. [64:14] uh it would be really great if we didn't [64:16] have to wait two years between you know [64:18] point releases of the big climate [64:20] models. Um so you know from that [64:24] perspect and to be able to you know get [64:26] an up-to-date view on the state of the [64:28] planet and and to be able to do [64:30] hypothetical reasoning about a policy [64:31] intervention that kind of thing. Um the [64:33] flip side of that is if you're doing you [64:35] know software engineering and you don't [64:36] want things to be changing constantly [64:39] that's where I look to this the unison [64:40] project. Didn't have time to talk about [64:42] it in depth but I encourage you to look [64:44] up um later. Uh they take seriously this [64:49] this sort of like versioning and [64:50] deployment problem um by basically [64:53] saying well old versions stick around [64:55] forever and you can refer to old [64:58] versions if you'd like and they're just [65:00] things with names that have hashes [65:01] attached to them. [65:03] And so you can be very deliberate about [65:06] the process by which you update existing [65:09] code to new versions, new versions of a [65:11] thing, right? Um, [65:15] you know, software engineering is as [65:16] important as ever having good processes [65:18] in your organization around when you do [65:20] that and how you communicate about that [65:22] and decision- making like we haven't [65:24] done away with for that kind of thing. [65:26] But the technical machinery that you [65:28] need to do that I think the Unison [65:29] project uh really has like done very [65:33] well and we're building basically [65:34] something based on unison there. Yeah. [65:39] Okay. [65:41] Great. Thank you all. [applause]