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