Future of Coding - Mathematical Foundations for the Activity of Programming: Cyrus Omar

Episode Date: June 7, 2019

Usually when we think of mathematics and programming languages, we think of tedious, didactic proofs that have nothing to do with our day to day experience of programming. And when we think of developer tools, we picture the practical, imperfect tools we use every day: text editors, build systems, libraries, etc. Cyrus Omar is new computer science professor at the University of Michigan bridging these disciplines by creating the foundations to precisely reason about the experience of programming. We open the conversation with how Cyrus got his start in computational biology, but how his dissatisfaction with the tooling led him to eventually to PL theory. At the time of this conversation Cyrus was interviewing for tenure-track positions, so we discussed the pros and cons of getting a PhD, being a post doc, and finding a job in academia. (He recently accepted a job at University of Michigan.) I enjoyed riffing with him on new media or platforms to accelerate science instead of the "dead tree of knowledge", including Cyrus's vision for a "computational Wikipedia" built on top of Hazel. Ultimately Cyrus shares the vision of democratizing computation, and we talked about how he imagines extending the Hazel project to be able to embed GUIs inside Hazel expressions, which can in turn contain arbitrary Hazel expressions or other GUIs. I loved our conversation about some of the classic touch points for improving programming - projectional editors, feedback loops, end user programming - but from a more academic perspective then usual. Hope you enjoy as well! Transcript at futureofcoding.org/episodes/039#transcript, provided by Replit. Support us on Patreon: https://www.patreon.com/futureofcodingSee omnystudio.com/listener for privacy information.

Welcome to the Future of Coding. This is Steve Krause. So one thing I've noticed in our community is that we all have our own peculiar interests, passions, visions for the future of coding, and also ways in which we think we can achieve that vision for the future of coding. And there are a lot of us who have different aspects of those visions and ways of accomplishing those visions in common. For example, I have a functional programming bent, and there are a number of people who are also interested in functional programming in our community. I also am particularly interested in democratizing programming to all sorts of people who aren't considered programmers today. And I'm also really concerned relatedly

to improving the programming experience of current programmers of today and also people who aren't programmers today but hopefully will be programmers tomorrow. And while there are a lot of people in our community who are interested in each of those things separately, it's quite rare to find someone who's interested in all of those things, really.

All of the ways in which I think programming could be improved and where we eventually want to end up with programming. One person that comes to mind that shares that vision for what programming could be and how we can get there is Paul Chisano, who was an early guest on this podcast and is also behind the Unison project. And today's guest is another such person who I share a lot in common with in terms of vision for programming and also how to get there. So if you are similar to me in some of these respects this conversation is gonna be right up your alley. So Cyrus

Omar is currently a postdoc at UChicago. He works with Robbie Chung and Robbie's team. And before that he was at CMU. And Cyrus' work is becoming increasingly widely known in our community. He's working on what he calls the Hazel Project, and it's providing mathematical foundations for the activity of programming. That's kind of how I think of it. The first iteration of this broader project is providing mathematical formal foundations for the semantics of incomplete programs. So one of the, I guess, shortcomings of classical computer science style semantics is that they only give formal meanings to complete programs. And the problem with that is that most of the time when you're actually doing the activity of programming, the program you're editing is incomplete, you know, because you're constantly changing it.

And so when you delete parts of that program, the whole program has no more formal meaning. And the tragedy here is that your IDE can no longer give you the good feedback you need in order to understand what's going on with your program until you complete the program in some way. You fix the syntax error or whatever it is that you're doing. And so what Cyrus' research, his initial research was focused on was how do we provide formal semantics for programs that aren't complete or aren't quite correct or don't quite make sense. And so he has this idea of typed holes, which I'll let him tell you more about in the episode itself.

So before I bring you Cyrus, we have a quick message from our sponsor. Replit is an online repl for over 30 languages. It started out as a code playground, but now it scales up to a full development environment where you can do everything from deploying web servers to training ML models, all driven by the REPL. They're a small startup in San Francisco, but they reach millions of programmers, students, and teachers.

They're looking for hackers interested in the future of coding and making software tools more accessible and enjoyable. So email jobs at REPLIT if you're interested in learning more. And without any further ado, I bring you Cyrus Omar. Welcome, Cyrus. Hi, thanks for having me. Yeah, I'm really excited to chat on the podcast. So I like to start at the beginning with these conversations. And so your background,

I think, was in biology before you found programming languages. Is that right? Yeah, I was really I was into neuroscience, you know, as an undergraduate. And I started my Ph.D. also in a computational neuroscience program. And, you know, I found myself kind of fighting the tools that we were using to do the kind of work we were doing more than I would like. And I've always had a hobby interest in programming languages and and and tools and and so I started doing side projects and those became my main projects and I decided I was actually in the I was in the woods for a summer I was at Los Alamos National Lab doing uh like a research internship thing there. And Los Alamos is in this forest kind of up in the north of New Mexico, up in the kind of the mountains. And I decided to just live in a tent

that summer because it's still kind of got this desert climate. It doesn't rain a lot. And so it gave me a lot of time for, you know, self-reflection. i uh yeah i decided you know building tools to you know multiply science would be a better use of my time than to just keep kind of unhappily doing science myself and so then i switched into programming languages at cmu which uh you know i was at cmu to do neuroscience i didn't really have any sense of like that. It was a good place to do programming languages research. And then I started looking around and I was like, oh, this is an opportunity to, uh, you know, be at a great place for this kind of thing.

And so I, I did it and it's been good. Yeah. Wow. You're quite lucky to be at CMU by chance. Yeah, basically. Luck is, luck is a lot a lot of, you know, a lot of our lives are ruled by luck, I think. Yeah, I think I felt like I had a similar luck,

I guess you could call it that, in that I didn't realize that Penn had a pretty good computer science programming languages department. But I later learned that it does because people often refer to um work done by the pen yeah no ben ben has really awesome pl so both we both lucked into being around fantastic pl people here we are there you go and i guess uh potentially we wouldn't have done it if if there weren't fantastic pl people around us subtly influencing us.

Yeah, probably not. So speaking about tools, I saw one of your, it seemed like one of your earlier projects was like kind of, it seemed to me maybe it was like inspirational for your current work um it was a project where you um took like a regular ide and then embedded like a regex playground and like also like a color picker widget inside of it what was that project about yeah so that was actually the first project i did when i switched into pl was uh yeah it's called um the tool was called graphite. It was this Eclipse extension that basically allowed you to use these graphical widgets to construct Java expressions. Those were two of the examples in the paper. There was a color chooser. The purpose of the widget was to generate code of the type at the cursor, right? So if you're trying to construct something of the Java class color,

what you could do is instead of writing new color and then the RGB values, you could use this graphical widget to select the color and it would generate the Java code for you once you press enter. And so that was one example. The regex thing was another example where it would generate the right regex Java value for you with all the escaping and everything done for you.

And what the paper was really about was extensibility mechanism to allow you as a library provider to define new, we call these widgets palettes. So these type associated palettes for the classes that you define. And so the paper was, yeah, I was actually taking a class at the time. It was a course project, and it was on human aspects of software development with Thomas Litozen and Brad Myers, who are really great kind of empirical PL people. And so most of the paper is really us. We did a big kind of 500 person survey where we gave people mock-ups of these palettes and asked them for both quantitative and qualitative feedback. And then we asked for examples of classes that they thought this might be useful for

and a few other questions like that. And we came up with this very, you know, interesting set of design criteria, this sort of classification of examples, and then a little bit of the paper was like we actually implemented it and did a little pilot study with it, but it was it was this kind of methodological paper of me learning how to do qualitative and empirical research that led to that project. And that project now is actually, so now we're revisiting that project in Hazel, which I can talk about it. I'm assuming you're going to ask me questions about Hazel,

but yeah, we're revisiting that project in the context of Hazel, which is a structure editor. So it's much easier to have graphical stuff integrated into the editor. Whereas in Eclipse and Java, it was kind of tricky to integrate the graphics into the text-based editor. So yeah, let me revisit that once I've talked a little bit more about some of the other things that we have in Hazel. Because otherwise it's

a little difficult to talk about what's new with palettes in Hazel. Yeah. Wouldn't that be funny if I decided not to ask you about Hazel in this conversation? Yeah, we could just talk about my first project from 2012 for an hour. That would be, there's a lot to talk about there. So I think, I mean, more generally, I think integrating, you know, GUI stuff with programmatic sort of coding feeling kind of stuff is kind of a frontier in both GUIs and in programming, right? I think in my mind, you know, when people think programming or when people think of

themselves as programmers, it's because they're writing code in sort of the textual style. But really, I think of any user interface as a programming language, right? So like Chrome or, or Microsoft Word or whatever, all of these offer you this, uh, set of primitives, which in, in word it's enter characters and open file and save file and copy and paste and insert image and so on. And these are all, you know, they're all functions. They take arguments, open takes the path as an argument uh and so i really want to take that idea and and run with it and really merge the uh you know return to the world where using a computer is programming a computer yeah i um i i see that vision as well. And I find that it's a very uncommon vision. Most people, like you said, think about programming as the superficiality of what programming is. person probably a like an asian or white man or an indian man like in a you know with a hoodie

you know with a green text and a black background and they're like doing their dark arts that's like and programming is related to like all of those things if you just say like well actually it's not it's not text and anyone could you know and more sorts of people can do it all of a sudden it stops being programming right it's interesting how that word has has evolved programming over the years and coding and now we don't really know what to call like using a computer used to be programming a computer and now it's now it's something that you know normal people use a computer and you know those kinds of people that you describe they program a computer i don't think that's right. Yeah. So I think that there is a true distinction between programming and using Word that you want to help blur that distinction or get rid of that distinction. You want to make

using a computer as powerful or as expressive as programming is. And so I'd be curious, yeah, to figure out where that line lies. Because in an earlier conversation I had on this podcast, I think it was Paul Chisano who said that basically it's just that the programming languages of Gmail or Microsoft Word are just, they're just bad programming languages. And so we just have to make our user interfaces better programming languages. Would you say that that's how you see it too? Just like adding stuff?

Yeah. In a lot of ways, I think that, yeah, that's exactly right. Like if you analyze the set of actions available to you in Word as a programming language, well, it's kind of an impoverished programming language. It's just some functions that you could call, but there's no abstraction mechanism. You can't very easily sort of automate repetitive tasks. And there's a very limited set of data types, right? In Word, you have basically strings, which are the text that you write. You have images, you have maybe tables of strings and images and a few other lists and things like that. But there's no way to talk

about the richer set of structures that exist in the world that exist in mathematics in word and um i don't think that's necessarily the way to design an authoring environment i think the way to design an authoring environment is to have it based in a programming environment where you have the whole the you know richness of mathematics there and then you layer on top of it the graphical elements that allow you to construct values of type string by just typing and construct values of type image by loading them from disk or something like that but fundamentally there's still those values and they can be manipulated programmatically and then the key is really to

be able to insert functions into into documents right So that it's not just these sort of base types in your programming environment, it's types that have an action on other parts of your document. And so that's how I sort of envision Azle actually eventually becoming an authoring environment with a programming environment environment sort of a conventional programming environment as part of its bigger kind of structure like the programming environments the base and then you and you build an authoring environment on top of it and and it's always kind of uh it's like a fluid transition from one to the other yeah exactly the authoring aspects of it are just a mode of use of these palace mechanisms, which allow you to manipulate certain data structures

programmatically, or sort of graphically. But underneath all of that, it is just values of various data types that you can also manipulate programmatically when the need arises. Fascinating. So I think the first time I came in contact with a vision of an authoring environment that was somehow more dynamic was, it may have been Alan Kay's Steps projects

or basically any small talky operating system world was where I first came in. Where did this vision come from for you um i mean yeah i i think i've read a lot about alan k's stuff so that's definitely part of it um the other part of it is just using like i read a lot about i i was really interested in wikis for a long time from the perspective of organizing science so when i started in neuroscience i was really kind of overwhelmed with the literature in neuroscience right like just in any academic field nowadays it's really quite difficult to get to grips with what's been done and to use what's been done directly right you have this kind of just

dead tree version of some piece of mathematics and you have to spend a long time implementing it to to get it to work in your project and so i uh yeah i became very interested in sort of reimagining academia in some sense as contributing to something like wikipedia collectively instead of contributing to something like Wikipedia collectively instead of contributing to this just like massive dead tree debris, right? And I thought, well, what would it take? Because, you know, what would it take to do that kind of thing? Well, there are lots of, you know, especially as a computational neuroscience, I'd read lots of papers with algorithms in them and math in them, and I wanted to be able to run those. So it was sort of obvious to me that this wiki would need to be a programmable sort of thing. And then when I switched to CS, you know, CMU is a very type theory heavy school.

So the first class that I took as a grad student in CS was a type theory class. Bob Harper was teaching it. And then it all kind of clicked. It's like types are everywhere, right? All the different types of things in your word processor are actually types. And I think it all just kind of flew like putting those strains, you know, trades of thought together kind of led to this idea. And it took me a long time to get to the point where I could start thinking

about it again. You know, that paper, that Palette's paper was in 2012, and then I spent a while doing other work, and now I'm sort of back to thinking about putting it all together again. But yeah, there's a lot of, I think a lot of different parts of my background sort of came together to make those ideas happen. Yeah, that makes a lot of sense. I really like that you brought up wikis and also collaborative science stuff because I don't think you and I have talked about it yet, but that's actually,

I'd say if I had to say like list my interests or projects I want to work on, like the first one is the future of programming. And the second one is like future of collaborative science. So maybe that's why we enjoy talking to each other so much. We have like the same top two interests. Yeah, exactly. I would say, yeah, those are, those are two of my top interests for sure. I think there's still very much a need for some, some way to get, you know, like to get

to grips with all of the knowledge that's been produced over the last several decades right i think having a place where you know we're all collectively trying to organize it is something that's badly needed and maybe we don't have the technology yet and that's what i want to work on yeah yeah yeah i feel similarly um yeah and i think I just want to point out one of the things you said there that I want to see. And I agree with you, but I'm not sure if I just want to point it out. You mentioned like a place and the assumption there is that like it's a single place. And I too get the feeling that something about that's important. So why do you think that's so important?

I'm not sure that that's strictly necessary. You know, you look at, like, I think of Wikipedia as the prototypical example of this massively collaborative effort to organize information. And it's such a tremendous success that, you know, to deviate too far from that model you better have a good reason i see uh but there's also a lot of excitement nowadays and and not centralizing resources like that and certainly you know it takes a lot of money to run wikipedia right and you have to donate to use it and so it's not clear to me that it needs to be a single place there's also different community uh standards right like wikipedia has a certain way that it runs its community and i know some people are not entirely happy with that uh and it seems like it's kind of premature to you know pick one set of rules for everybody

and so i definitely want whatever we build to be for it to be possible for someone to run their own instance of this and and and compete or target it towards a different community or use it for some kind of a small subculture but i can also imagine it being one place like wikipedia where you know people are collaboratively writing the encyclopedia of you know computational uh the computational world which is increasingly the whole world. Yes. I want to throw one more thing, one more idea out there about this, and then we can go back to programming. So in the same way that you want to blur the line between using a computer and programming a computer, and like instead of programming a computer being something that you have to

like wear a special hat or hoodie, I guess, in the case of programming, you can something that you have to like wear a special hat or hoodie i guess in the case of programming you can just you know wear whatever clothes you want you can you can do it yeah um i feel like with this tool for science could enable is a similar kind of blurring so you don't have to wear a lab coat anymore to do science and contribute to like humanity's collective uh scientific knowledge like Maybe this kind of a tool could be a workaround and get away from the like ivory tower of like papers and like all the artificial gatekeepers and somehow democratize science.

Do you feel the same way about this medium? That makes me feel good to imagine that that could be true it definitely i want that to be possible but i also i mean i am kind of deeply enmeshed in academia and i see how much money and time it takes to do good work and so, and especially, I mean, in biology, you can't, you can do theoretical biology just with a computer. You can't really do experimental biology in your basement right now. You know, there are some efforts to kind of do some stuff and, you know, some experimental biology kind of kits and stuff exists but it's really hard to imagine the kind of work that happens in neuroscience happening without institutional support and you know in some other areas in computer science generally outside not you know not not biology or something like that

people developing algorithms yeah that's definitely what i want i want it to be democratized and i think increasingly that's happening i think a lot of really cool contributions in computing are happening from people doing it in their off time as programmers in industry. But I still kind of struggle with that idea as kind of a way to do things like biology and chemistry and experimental physics and things like that so alternative like funding models and and research lab models and things that aren't so tied to the academy could work and i think there are some examples of that happening yes in neuroscience you have this place the allen institute Institute, that Paul Allen funded, which is just kind of an independent research institute that does a lot of neuro, they call it neuroinformatics.

So like developing digital resources for neuroscientists, databases and things like that. And so that, yeah, that's the kind of thing I want to enable but the conversations still need to happen about how to like break free from the current institutions because they have billions of dollars going into labs and and experiments yeah yeah well I feel like the funding maybe is kind of like an orthogonal concern. Well, it's obviously like deeply embedded, but anyways. Yeah, I hope the more it's an orthogonal concern, the better. Yeah.

Yes, yes. Well said. So anyways, enough of us having fun. Well, we can still have fun, but let's talk about your main work. Yeah, serious. Let's talk about those Greek letters that you've got. Well, yeah. So my main project, which I've alluded to, is called Hazel. And it's really kind of an experimental platform for this theoretical work that we're doing,

which is so far focused on this question of understanding incomplete programs. So programming languages have typically kind of defined, programming languages and compilers, implementations of programming languages, right, have typically restricted themselves to understanding complete programs, meaning programs that can be parsed according to the grammar of the language that can be type checked successfully according to the type system of the language and that can be run without kind of failing. And those are things, those are sort of what we want to produce at the end of the day when we're programming. But during the actual process of programming, this sort of act, this, this dialogue that you have

with your programming environment, you're not producing complete program after complete program. You are in the, in, you know, in these incomplete states where there might be missing chunks of a program, where there might be errors that you're, you're puzzling about, um, where there might be multiple people working on different parts of the program, and so they're inconsistent temporarily. So we haven't really had a foundational theory for incomplete programs. There's been bits and pieces of theory, but we really wanted to develop sort of the lambda calculus of incomplete programs, where the lambda calculus I think of as the, you know, Schrodinger's equations of computer science. It tells you what abstraction is

fundamentally without introducing anything else, and then you can layer on top of the lambda calculus any other language feature that you'd like in this very nice orthogonal way where you can then study that feature in isolation. And so that's what we want to do with the foundations of Hazel, which we call Hazelnut, this core calculus that is based on the lambda calculus that allows us to work with these incomplete programs, which are programs with holes. So there are empty holes in Hazelnut, which stand for missing parts of the program. So missing expressions, missing types. We just added pattern matching actually to hazel,

so missing patterns as well. And then there are these non-empty holes, which serve as membranes around erroneous parts of the program. So type inconsistencies, finding errors where you have an unbound variable, for example, other things like that. And so the last two years have really just been figuring out how to reason about these incomplete programs in this lambda calculus setting, meaning developing a type system for them and then figuring out how to run these programs. So I just came back from POPL in Portugal

where I presented a paper about how to run incomplete programs. And the idea is you want to get feedback about the behavior of parts of the program that you've written before the whole program has been written. And so conventional programming languages, especially statically typed programming languages, have not been able to do that. They just don't let you run the program until it's completely complete.

And we developed a theory and implemented it in Hazel that allows you to run the program before it's done. It'll sort of evaluate everything around the holes in the program and track some environment information around those holes to allow you to see the values of the variables that you've found so far while you're figuring out how to finish the program. And so yeah, so Hazel's really this almost a philosophy of language and tool design right now where we say let's figure this stuff out in a very simple setting and then start implementing it from there. And now, the last few months have

really been focused on scaling that up. And so Hazel is, you know, it's still a very simple programming language and programming environment. But it's, it's sprouting more and more features like those you'd find in full-scale functional languages right now. So we're kind of targeting Elm because it has a, you know, it's a pure language. It doesn't have exceptions, so you don't have to deal with programs crashing because exceptions weren't caught. And it's a language that's used by a lot of people in the web programming space. Hazel is a web-based tool and so that's kind of what we're initially targeting.

But really we're using it as a place to explore even language editor co-design kind of questions like are there features you don't need because you have editor support, are there features that work better because you know that you have an editor of a certain kind. So those are the kinds of questions that we're thinking about right now. Yeah. Fascinating. There's so much I want to reply to. Yeah. That was maybe too many things all at once, but. No, no, it's great. I love it when I interview someone and I know they have a spiel and then I can

just, you know. Yeah. Yeah. I've been writing a lot of research statements and those kind of things lately. So I've practiced. Yeah, well, and I could even tell when you gave the presentation at live. I feel like you were the one guy who got up there and was just like, like, I've given this talk a bunch of times before. Like, I know how to explain what I do.

Yeah, I mean, I've presented. Yeah, LaFalle was a lot of presentations. I went to Strange Loop and I went to Live and I gave some talks at universities. And so that's what you do as an academic, right? You like give talks so that people take your ideas and run with them because I don't have a massive engineering team.

I just have ideas and freedom to explore those ideas. So I'm going to try and remember the things i want to touch touch on the first thing that struck me was that the lambda calculus is the schrodinger schrodinger's equations of programming yeah and so i computer science oh of computer science i see yeah well there's a difference i there the first thing that comes to mind is I saw, I think it was Alan Kay who said that it was the initial definition of Lisp in Lisp. He said that was like

the, I don't know if he said Schrodinger's equations maybe he had a different... Yeah, I think I've heard people talk about there was a blog post I saw that was like here's a minimal Lisp interpreter and we should think of this as the Schrodinger's equations of programming or something like that. Well, and I guess is Schrodinger's equations important, or could you say, I think maybe the Lisp one was Maxwell's equations.

Oh, Maxwell's equations. Sure. So it doesn't really matter. It doesn't matter. Which set of equations. You're just saying it's like the foundational set of equations for a field. Yeah. Yeah, i think so um i don't think there's really a tension between saying it's like you know lisp at its heart is the untyped lambda calculus so uh okay you know it's a matter of notation almost yeah oh okay that oh okay so they really are equivalent in that way that's interesting well i don't know what people mean when they say that, but in my mind,

I think of the untyped Lambda calculus there as being the foundations of these kind of classic Lisp systems. Are there other foundations for programming that are in contention with Lambda calculus? I know there's a Turing machine but i but people don't use it for i i imagine for good reasons um are there other calculi that are competitive or it's everyone pretty much agrees that the lambda calculus is the way to go um i think everyone pretty much agrees that the turing machine is the way to go and i think they're probably wrong um yeah i don't know i uh i live in a world where everyone agrees that the Turing machine is the way to go. And I think they're probably wrong. Yeah, I don't know.

I live in a world where everyone agrees that the Lamb of Calculus is the way to go. But the world's a big place. Oh, I see. I don't want to characterize other people's opinions on this. Well, I guess I'm talking about the world of academia. Because I guess that was... And even in academia, there are multiple worlds where some people are lambda calculus people and others aren't for sure yeah i mean the lambda calculus is very austere and it doesn't capture imperative programming by itself you can extend it to capture imperative programming but it doesn't initially capture state. And of course, state's a big part of how programming is done today. And so there are other abstract models of computation where

state's much more central, like the Turing machine, and people use them for different purposes. Yeah. So anyway, the language calculus works for me really well in terms of when I think of a new language feature, if the first question is then, what would that feature look like as an extension of the simply type lambda calculus? You get a lot of mileage out of that way of thinking. Yeah, yeah. And I have a friend actually who speaks in a very similar way. And I forget. There was a speaks in a very similar way. And I forget. There was a book he told me to read.

I think it may have been written by Bob Harper. Was it Practical Foundations for Programming Languages? It has one of those titles that's impossible to remember because it's just like, you know, the name of the field and the word like practical or something. Yeah. It's probably that book. Yeah. So that's a great book. That's the book we teach our PL class out of at CMU.

And it's yeah, it really, it starts like from the simply type Lambda calculus and it builds up kind of this, all of the features of modern programming languages as extensions to the Lambda calculus. And it's really beautiful, right? Every page, you know, all of the features of modern programming languages as extensions to the lambda calculus and uh it's really beautiful right every page you know you have just two or three pages which get to the essence of concurrency and lazy computation and uh imperative programming and and all sorts of other things right there's like 40 or 50 chapters in this book and they're all a few pages long and they're so you know they're so insightful so sorry is this the one tapple is

that how people refer to it uh tapple is a different book that has sort of a similar feel tapple's a little older book by uh benjamin pierce at pen so you got it you were exposed to that i see and uh yeah pfpl is kind of the abbreviation that people use for this bob harper book yeah so i don't know if you know steven deal um from from places on the internet yeah i know i'm from twitter yeah yeah yeah so he we met up because we're both in london and he's he's been pushing both of these books on me for and for similar reasons that you alluded to. The idea of if you're a programming languages person

and you want to be able to test out language features in isolation, this provides the tools for you to do that. Yep. Yeah, exactly. It gives you this way to kind of just isolate that feature and talk about it very precisely, right? You can say, what are the theoretical properties of this feature? What invariance are you going to be able to state about the lambda calculus extended this feature? Which is something you can't do without a foundation like the lambda calculus in mathematics, right? A

foundation in mathematics. So Bob likes to call like the alternative approach where you just kind of implement stuff in your favorite interpreter, uh, seat of the pants programming language design. Right. It's just like, let's see what happens. Right. Like, I don't know. I don't, I'm not going to prove any theorems. That's, you know, that's Greek and I don't speak Greek, but, um, then you end up with these misfeatures, right?

These features that you regret and they're kind of stuck in the edifice of computing now. It's like null pointers, which, you know, the designer of that feature now regrets and it's called the billion dollar mistake. Right. Um, so yeah, it gives you this, this process that ends up with you feeling very confident about what it is that you're doing. It's not just flailing around in the dark as a designer. It's really mathematics informing design. And, you know, I think it works really well. thematics informing design. And, you know, I think it works really well.

I think languages that are, you know, rooted in this process are now starting to reveal themselves as languages of the future. That's a contentious statement, but. Oh, it is, but no one else is here to argue with me, so. That's true, especially because i agree with you so i'm not going to argue with you um so um to get back to some of the things you mentioned um i i don't know if you mentioned this phrase uh in in your your spiel just now but i've heard you you refer to it before, the gap problem. Yeah, the gap problem is just, I mentioned, I didn't say that phrase, but the gap problem is just this gap between times when your editor is in a complete state, right? So when you're typing,

you might write two plus, and in that millisecond before you write two after the plus your editor actually can't even parse what you wrote right so it's quite hard for it to suggest something for you because it can't understand what you're doing and so the gap problem is refers to these gaps in service gaps in editor services that arise because it doesn't have a an understanding of some of these editor states that arise and so that example was the gap is very short but there are examples if you've been doing a long refactoring right if you change a type definition and then you have to go change you know 200 different places in the program while that whole time you're doing that, you certainly can't,

the program doesn't type check, you certainly can't run it. Sometimes it won't parse. And so with Hazel, we've solved the gap problem in the sense that every editor state, you know, every key that you press in Hazel produces an editor state that is both statically meaningful,

meaning that there's a type assigned to it, that type might have holes in it. And it's also now dynamically meaningful, meaning you can run it and get a non-trivial result out of it. And so that's kind of the calling card of Hazel is no gaps, right? And that's what we're trying to maintain. Not a few gaps, but like no gaps, right? And I's what we're trying to maintain. Not a few gaps, but like no gaps, right? And I think that doing a clean slate design

is really what enables that for us. Yeah, I like that, the no gaps idea. It kind of reminds me of if you put like a monkey at a Microsoft Word and they just hit on the keyboard, it would just show something. It wouldn't make sense, but it wouldn't just show something it wouldn't be it wouldn't make sense but there wouldn't it wouldn't like just you know it wouldn't just show you errors it would show you whatever the monkey

pressed and so hazel has that property of you could put a monkey in front of it and it'll like still have no gaps it'll still like give the monkey good editor services yeah i like to use in my talks i have this uh image of a cat sleeping on a keyboard and having typed out some nonsense. So even in those situations, exactly, like you get feedback about what happened. It might be that the feedback that you get is just that this makes no sense, but at least to the editor, it makes sense. And that allows it to help you get it to make more sense to you and i think a point to just

make clear is that even if like the monkey by accident put like six plus and then and then some garbage or six plus three and then plus and then some more garbage it would evaluate the six plus three correctly in the context of garbage uh so i think that's like a really cool property yeah exactly if you have a little type error after this, if you write six plus three plus F and you're about to call F, but you haven't yet, that's a type error. You wouldn't be able to run that in pretty much any programming language today,

but in Hazel, you'll get the nine plus F and the F will be in this non-empty hole, which is rendered as just a dotted red box in the way that you're probably familiar with from even Microsoft word, right? It's like a spelling error, but it's a type error.

Yep. Yep. That's, that's another great metaphor. It's yeah, just, you just underline the errors and just leave them there because they don't stop anything.

Yeah. It's like reifying the errors is what we're doing, right? They're not just part of the display. They're part of the semantics of Hazel. Yeah. That's a good way to put it. So I feel like what you're almost doing with this argument of the gap problem

and these editor services that are so important and how you're able to solve the gap problem and provide editor services forever, as long as you have this editor semantics and a structured editor, I feel like you're kind of building up to like the ultimate rigorous defense of structured editors. And I feel like the, this conversation has been lacking up until now. People give some benefits of structured editors. Other people say, Oh, well, we tried those before they didn't work. They're never fluid, but I feel like you, you're almost in a position to make like a crystal clear

case of why maybe we aren't there yet but in the future this is going to be the way to program yeah so what structure editing buys you hazel's the structure editor uh what it buys you is so I mentioned these holes right these holes are what allow you to represent these incomplete programs instead of having nothing there it's like the concept of zero in mathematics right for a while I guess people thought why do we need zero it just means nothing there it's like the concept of zero in mathematics right for a while i guess people thought why do we need zero it just means nothing right that's actually very important to have zero and in the same way it's very important to have these holes that like positively represent

nothing being somewhere and uh what structure editing allows you to do is it makes it so you, the programmer, don't have to insert the holes manually. So like in Haskell today and in several other programming systems, you can insert holes manually to make the type checker happy. Structure editing inserts holes automatically, both empty and non-empty holes automatically. And so that's what gives you this full end-to-end kind of solution of the gap problem is there's never even these states where you haven't inserted the holes in the right place. They're just always inserted where they need to be to make the semantics happen. And I think there are, yeah, so you mentioned, I mean, there are structure editors have been around for a long time. You know, we didn't invent the concept of holes or anything like that and hazel uh what there are yeah there have been lots of questions

about the usability of these things um you know you can easily get yourself into a situation where if you're trying to say every single editor state must have these very strong properties then it makes it very difficult to program fluidly because you do naturally sort of go through these intermediate states when you're programming in text that don't make any sense. You know, two plus F, maybe you're about to apply F, but that moment doesn't make any sense. Yeah, I think it's even stronger for me when I'm like trying to mess with parentheses. I like take something that was like an outer thing and trying to make it an inner thing. Or I'm like doing a refactoring where I'm really like inverting the control structure.

Then like there's a lot of states that just don't make any sense. Right, exactly. So I think that's still an open question, right? I think there has been actually some really interesting work fairly recently in this project called Embedder, which is built using this tool called MPS that JetBrains makes, which is a structure editor generator sort of, and Embedder is the C-like language not only for embedded systems that is a structure editor, but it gives you an experience of programming that feels a lot like text it just feels like you're writing in a language with holes and it's just

inserting the holes automatically but otherwise the experience is quite text-like and it does that by representing in the AST these sort of weird states where the parentheses aren't balanced it's just like okay that's the kind of node unbalanced parentheses node whoa that's interesting yeah so uh so we've been taking a lot of inspiration from that that design in hazel so hazel's also kind of designed not not to be this you know there are structure editors that are like these blocks languages that kids use to learn programming like scratch um those are also structure editors, but they aren't very fluid, right?

You wouldn't want to use those as a professional developer. We're really targeting more of the like, not entirely professional, but like adult programming. And we're inspired by this kind of hybrid approach where it feels mostly like text except there's holes inserted automatically. And then we're exploring this idea of text edit holes which basically say if you do find yourself in a situation where the available structural actions are not satisfactory, right, that you can't figure out how to make the refactoring happen

that you want to have happen, then you can say figure out how to make the refactoring happen that you want to have happen, then you can say take this subtree of your program, temporarily render it just as text that you can edit as text, and then but from the perspective of the rest of the program, it's just a hole that you're filling sort of with text. And so it doesn't make the whole program text it just makes a subtree text and that's particularly helpful if you want to work collaboratively with people where you don't want some edit somewhere else in the program to make your whole program meaningless so that's some that's an ongoing kind of thing that's not in Hazel yet, but we're thinking about how to do that right. It kind of, like, you're technically, you've still solved the gap problem, but in that subnode, you don't actually get editor services.

Right, yeah, or you just get the kind, you know, you get maybe syntax highlighting based on regexes like a lot of editors do, but you don't get the full full suite of editor services yeah yeah well to me that feels like a stopgap solution like one day hopefully we'll have solved the fluid structured editor problem and then yeah you'll get you'll get rid of that escape hatch yeah it's definitely a stopgap. And I think, yeah, that's that, um, another project that we're working on is, is, uh, user defined edit actions. So you can imagine edit actions that are much higher level or that are very specific to a certain API that take advantage of like the algebraic properties of some structure in a library that you've defined.

It'd be really cool if importing that library also imported some very domain-specific editor actions. So there's been some cool work in Idris on these kind of ideas, and we're kind of trying to take them further and develop the theory in Hazel for that as well. And so eventually, yeah, I hope that those kinds of features allow you to avoid needing to drop into text very often and maybe at all eventually.

Cool. In terms of editor services and the gap problem, one thing that comes to mind is hot reloading. Are you familiar with that term? Yeah, yeah. So I guess, sorry, yeah. Go ahead. Did I lose you for a minute there? No, I'm here. Okay, so hot reloading,

I think where I first heard the term was in the context of front-end web development. If you have a complicated app and you're developing it and there's a nested bit of state where you have to click a bunch of buttons to get to a window where you're trying to actually develop. And you hit save and you have to reload the whole page and re-navigate to where you want to go. It's annoying. So wouldn't it be neat if we could just hot patch the changes to your app that's running?

You get where I'm going with the question of the problem with hot reloading is that it's unbelievably messy. And so you end up in all these weird states. And so what I feel like the space of hot reloading needs is a similar kind of semantic foundation. So you can do this

in a way that's always safe. Is that something that this will help with? Yeah. So we've worked on that in the same paper that did the live programming. So we have a little section on what we call fill and resume. So what happens when you have a hole in your program, you run it, is you end up with a result with holes in it uh corresponding to holes in the original program and uh if what you then do is go back and use that additional feedback that you got from running that incomplete program to fill in one of those holes while you want to be able to continue evaluation from where it left off where it sort of had to stop because the holes were in places that where it needed to know what was going to be in the hole to continue and um so we developed a

semantics for uh resuming evaluation where there's a theorem that says that the result that you get from resuming is the same as the result that you would have gotten from restarting yep yep and and that that's exactly what i'm looking for that gives you this confidence that you know you're not reloading into a state that you couldn't have ever gotten into from the from the beginning yeah so if you think about like if you've ever used like jupiter or ipython this is like lab notebook things where you have these cells with code in them uh you can find like what you can do is you can it's kind of like a rebel except you can go back and re-execute a cell and what happens is that the order that you as the user sort of interact with the gui to

re-execute cells will change the state of memory in your in your notebook it's awful and it's yeah it's totally awful right like you end up sending the notebook to somebody else. They run it from the top on their machine and they get a completely different result. And it's not reproducible. If you're doing this in science, it's kind of a disaster. You want it,

you want your, you know, analysis to be reproducible. And so this guarantee of, uh, we call it commutativity. So what happens is what's commuting is editing is commuting with evaluation whole filling in particular is commuting with evaluation so yeah having that guarantee i

think is a really important guarantee for reproducibility and sharing code with other people performance and so on yeah yeah what it doesn't do is it what it doesn't do is allow you to change the code in ways that don't amount to hull filling. Oh, interesting. Yeah, that's what I was going to ask. Yeah. So, I mean, that's trickier because if you've actually just changed the behavior of the program is different all the stuff that happened before that you want to avoid rerunning would have happened differently because the code is completely different so it's trickier to get that kind of guarantee you can certainly there are there are you know

hot code reloading mechanisms that try to protect you from really egregious changes in the way your stacks and heap is laid out but it's not it doesn't have that kind of strong guarantee anymore well i feel like the same way that you justified and and like contextualize what you've done with typed holes you're like well we used to only care about programs and now we care about programming and like incomplete programs. I feel like you could say the same thing about how we don't care about complete programs. We care about like programs that change over time because that's what programming is about. So even if I have like program A and it's complete, there are no holes, like p prime and p prime prime are

like fascinating because you know that's what the dialogue is about i'm constantly changing yeah and so i feel like there should be some semantics um there's some should be some semantic foundation of of evaluation of p and i change it to pre-prime and like i still have the evaluation of p there should be some way to save the part take the diffs and apply them have the evaluation of P, there should be some way to save the part. Take the diffs and apply them to the results somehow. Yeah, there should be some way. Or, I don't know, do you think the same? You get what I'm getting, the parallel I'm trying to go for.

Absolutely. So there's this area of PL research called incremental computing. And there the idea is if you have a function and it takes similar inputs to similar outputs in some way, then you should be able to take the diff of the input to the function and sort of apply a patch to the output that takes less time than rerunning the function again. So there's lots of interesting work in incremental computation that gives you ways to do that for different classes of data structures using different techniques some static some dynamic the complementary question though is what you're asking is what if it's not the input to the function that's changing what if it's the function that's changing yes and i don't know how much work has been done on that. Maybe some. I'm not 100% sure.

It'd be worth looking into. But it's a harder question because it's like the entire trace of the computation is now going to have changed because the body of the function is now different. And so you can try to do some checkpointing kind of things where you say, well, until you get to the code that changed, everything was fine. And until you get to it in the control flow, you can like reuse kind of a prefix of the trace control flow what is that there's control flow control flows are when you take a branch in a case analysis that's just data flow yeah that's fair yeah so i don't know yeah i think that's an interesting Yeah, so I don't know. Yeah, I think that's an interesting set of questions.

It's worth investigating further. Cool. And do you think it could be investigated in much the same way that you did your typed hole investigation? Like in the type lambda calculus, like language extension? Oh, yeah, that's the only way to do it. Okay. I mean, you could do it by the seat of your

pants but you know we're we're many decades into computing now i think it's time for us to return to some principles okay yeah um all right so there i have a few more questions um so one of the questions um or something that someone said when I showed them the Hazel work, they like looked at it for a second and they're like, isn't a hole in a function that I'm not totally complete with just a parameter? Just like, can I just wrap the whole thing in a function and call that a parameter? Is that, yeah. So yeah yeah what's the response yeah so a parameter is mediated by a variable and when you fill a hole it's not exactly the same thing as substituting for that variable because substitution is maybe i'm getting too wonky here substitution is capture avoiding see

you you when you fill a hole you won to have access to the variables in scope at that hole but a parameter to a function doesn't have access to the bindings inside that function right that would be kind of a treacherous violation of the binding discipline of most languages so they're not quite parameters there's this notion in type theory in particular this kind of type theory called contextual modal type theory called a meta variable and a meta variable is kind of like a variable in that it has a type but it also has a context associated with it which is the set of bindings in scope at that meta variable and you don't substitute for meta variables you instantiate them which means uh you feel you replace the meta variable with an expression that has free variables in it that get

rebound in the scope of the variable, of the meta variable. So like, yeah. So your friend is sort of on the right track, like there is a relationship to something kind of more well understood, but that something is called a meta variable in contextual type theories and our paper at popple goes more into that and so just i'm going to try and repeat it and maybe i'll get it right or wrong a meta variable is like the context uh like the and when i say context i mean the all the variables that are in scope and their current state so is that what a meta variable is basically yeah it's just context yeah so the way you refer to a meta variable is with a quote like what's called a meta variable

closure which is for all the uh variables that that meta variable, that the thing that the meta variable stands for might use, there has to be some value for that. Yep, yep. Or some substitution for it. That makes sense. Like the this keyword in JavaScript kind of closure-y thing. Sure. This keyword in JavaScript.

That's why I think of it just like as a function closure, in that you take a function value and it's all the environment around it that might be relevant to that function yeah the only reason that javascript comes to mind is because sometimes when you write a function you want to specify what environment you want it to evaluate in like what context like what you want it to close over i see okay and so sometimes in javascript you. And so sometimes in JavaScript you'll pass it. You'll pass it an object that will act as its environment. Oh, I see what you mean.

Yeah, this is giving you the implicit, like when you refer to something not in scope immediately and that function goes through this, I guess. It's been a while since I've written JavaScript. Well, yeah, you're right. I'm not exactly sure either what I'm getting. All I know is that you can change the meaning of this by specifically saying... Like doing this dot apply thing. Yeah.

What is it called in JavaScript? Well, I know that with the fat arrow, it does automatically. Mm-hmm. I think maybe dot bind. Yeah, there might be some relationship there. Yeah. Anyways, yeah. Like rebinding this yeah yeah um

yeah i mean the real kind of elegant relationship is with this contextual modal type theory which is um which is a a type like a proof theory for this logic called contextual modal logic which there are all these different kinds of logic that philosophers came up with long before computing right and um this particular logic talks about necessity like it's sort of the analytic philosopher's way of talking about what's necessary for this thing that i'm talking about to be valid and for a meta variable it's like it's necessary that whatever you fill me with better have this type using these variables and so it gives you this really nice connection to the history of the world before computers

that's what i find really nice about these logical connections that when you discover them you know that there's like some concept that's independent of the like details of the computer industry that you've discovered yes i i want to get more into that later like the generality of theory um i'm excited to do that um But I just want to finish up with Hazel. Let's see. One of the things that you alluded to that I want to get back to is the palette work that you started your career with. Yes. Yeah. And so part of why I brought that up initially was because I think it's relevant to how you started out with building these GUI augmentations to a Java IDE. And then my guess is that part of what you ran into is that what was so hard about building those,

one thing that was hard about building those sorts of augmentations is the gap problem. Is that where you first ran into it? And then that's kind of what inspired this project or am I just projecting your experience? Yeah, sort of. So like in Eclipse, like the way the palettes, sort of. So like, in Eclipse, like what, you know, the way the

palettes were sort of presented to you was based on the expected type of the cursor. But of course, what that requires is that there, that has to exist, that Eclipse needs to be able to tell that to you. And if it can't even parse your program, it's hard for it to do that. So what Eclipse does is it actually doesn't solve the gap problem, but it uses these very complicated heuristics to try to sort of internally insert holes. You can think of it as internally inserting holes to be able to offer you that kind of expected type when you've just typed like f open parens. That doesn't parse according to the grammar of Java, but Eclipse doesn't completely barf, it just it says i have this heuristic for that particular situation where there's an f and an open parens where i'm

going to tell you the type of the first argument of f and eclipse and other sort of industrial grade ides are full of heuristics like this right these code bases are millions of lines of code of heuristics and they manage to sort of work most of the time and that's how that that heuristic is what we rely we rely on eclipse just having this type information available from its own internal heuristics to be able to invoke the palettes uh in hazel we don't have there's no heuristics right there's just a nice elegant simple theory there's not millions of lines of, there's no heuristics, right? There's just a nice elegant simple theory. There's not millions of lines of code, there's just thousands of lines of code. And yeah, so then the palettes, what was limiting in the Eclipse setting with palettes, there was a few things that we're trying to improve with palettes in Hazel.

So one is, palettes in Eclipse are ephemeral. So once you're done interacting with the palette, once you've written your regex in your tests, or when you've selected the color that you want, you press enter and it generates Java code. And then that's what's in your file is the generated code. And that's fine if you made the right decision the first time, but it's not great if you want to change the color or you want to edit your regex and bring the tests back up. And so in Hazel, because you're editing in AST directly,

you don't require it. It's not just a textual representation. The palettes are part of the program permanently. They're generating code underneath of them, and there is an underneath, right? There is that dimension of things that are in the program that we're not showing you right now. Instead, we're showing you the GUI on top,

and you can flip to the thing underneath if you want. And so that's really much easier to do in a structure editor than it is in a text editor. It's not impossible to imagine doing that in Eclipse, right? You could try to put overlays and things that change how things are rendered, but it's much more difficult to do when you're sort of trying to turn Eclipse into a structure editor at that point. So for that regex example, if you're in Hazel and you write a regex, you write some test examples and you're going along, where are you storing those test examples?

Is it like some metadata attached to the language somehow or it's like there's a yeah how does that work so each palette is written uh each palette is kind of a little mini elm program in a certain sense it has an abstract model which is what's persisted in the ast and then it has a view function and some other things to display the GUI. And yeah, the AST just keeps track of that logic for viewing things in this palette context. And then in the AST itself, at the place where the palette is generating code, it's just keeping that model. You can think of it as a serialized version of that model although There's not a lot of actual serialization necessary Because it's just a hazel value

Yeah, so that's that's the design that we're working on right now is in the AST if you just looked at the AST kind of abstractly, it would be the name of the palette and the model. And then the UI of Hazel passes that model through the view function and renders the view. And then the activity of the view called expand that takes the model and generates hazel code which is what is what the meaning of the semantics of that palette is is the code that generates oh okay so if you have a palette in the tree there there doesn't exist the expanded code by itself. Right. So you can, you can cache that.

I mean, there's performance things you can do to cache that expansion for a given model, but like abstractly it's just the model. And then there's the palette has some logic for turning that into code and turning that into a view as needed. That's very cool. So I guess you could implement it in a bunch of different ways,

but what I like about the way you implemented it is that it makes it very clear that this GUI thing, like it is the canonical representation, and then the expanded view is just like something it produces. Yeah, exactly. So this is closely related to some recent work I did on literal macros in Reason and OCaml. So you can think of these palettes as kind of graphical literals right. You know like a list literal is kind of a one-dimensional GUI for lists right.

And imagine you want a matrix literal that's like two-dimensional, then you can do that with palettes. And in fact a lot of the same theoretical considerations that come up with how to generate these expansions hygienically, because it's a macro system really, and how to reason about the rest of the program in the presence of these palettes, right? Because what, you know, if you're not seeing the expansion, how do you reason about what the program's doing? Well, there are some ways to do that in the context of type macro systems that apply also to this palettes mechanism. And so yeah, I think of them as kind of graphical literals. And then, yeah, that brings up another thing

that we're trying to add, which is you might want expressions inside the GUI. Yeah, you took the question right out of my mouth. Yeah, yeah. So that wasn't something that in the Eclipse palette mechanism that you could do. So you could go from code to graphics, but you couldn't then inside somewhere in the GUI

go back to code. And that doesn't work great if you're, for example, as a matrix palette, you want the elements of your matrix to be expressions in your programming language, not just literal numbers. So in Hazel, we're having it be totally compositional. So you can have these holes inside the GUI, which can be filled with Hazel expressions. And one form of Hazel expression is a palette expression.

And so you can nest palettes by going sort of into a palette, then back to Hazel, and then into another palette. So it's like in and out. When you say in and out, you mean your cursor can go in and out? Or you mean that you can't, like, can it look like a nested structure where I can see an outer structure and then it's like an inner structure? It's like nested boxes all on the same screen and my cursor can just move fluidly? Yeah, nested boxes, basically. Yeah. So, like, you can imagine there's a palette for generating numbers by manipulating a slider, right? Really simple example

then you can have a matrix of sliders right you'd want to be able to do that and then what if i want a matrix of sliders and each slider is multiplied by 10 you know like can i can i do yeah yeah mathematical expressions you can put that slider anywhere a number is expected so inside an arithmetic expression it can be like slider times 10 perfect yeah beautiful yeah oh wow there's some questions about how to lay out stuff like that once it gets really deep and uh yeah layout is tough question actually but it's actually working. Yeah, well, so, well then like all of a sudden you,

it like begs the question of what is the difference between a expression and like a GUI? And I feel like that a, if layout happens automatically, then it's like you've just augmented programming with some literals, and that's neat. But I feel like if you give people full expressive control over the layout, then all of a sudden you've done it. You've blurred the line between GUIs and programming. Yeah. Yeah. it you've blurred the line between GUIs and programming because yeah yeah well you can imagine a layout manager palette whose only purpose is to take a bunch of sub-expressions

and lay them out according to some rule specific to that palette the way many GUI frameworks like for iOS you have these different layouts so I think you can already kind of imagine doing that without any special mechanism in Hazel. It's interesting because to me it feels like almost like macros because if you have an expression in code, you don't think of the expression itself as data. You just think of it as, well, usually you don't think of it as data. But when all of a sudden the expression is GUI things and you care about the way they are laid out, then all of a sudden you want to be able to manipulate these things as data.

So that's fascinating. Yeah, it's definitely very, I mean, macros are the foundation for this mechanism. It just adds a bunch of stuff. And then the other, yeah, the last thing I wanted to mention about what we're doing with Hazel and palettes is if you have a hole in a palette, for example, okay, so here's an example of a palette that's kind of interesting. Say you're constructing a plot and a plot has a title and has axes labels and it has some data and it has some color parameters for different lines and so on and those are all things where you can imagine like maybe it's nicer

to directly manipulate that that plot edit the text and and the colors and stuff in line but the purpose of the plot is to plot some specific piece of data right like you can create an abstract plot with some abstract data and then run that program and get the actual plot, but it'd be nice if you could actually see the data itself that you're going to plot as you're manipulating that plot in the program, a sort of plot constructor in the program. And so, well, I just talked about you can run incomplete programs and you get these holes in the result with these closures around them that give you the values of all the variables in scope. Well what if we ran the program where all the expressions that the

palette's generating are just temporarily holes and we gather the closure information around them and then we provide that closure information to the GUI, to the palette. So then the palette could say, OK, well, I know you want to plot this particular piece of data. I'll just show you it right here in the middle of your program instead of waiting for you to run it and seeing it at the bottom of your program or wherever. And so having these live palettes that really have access not just to the abstract expressions that you've entered inside the holes, but their actual concrete values,

if they're available, is something that we're working out how to do right now as well. And it's really based on the work we've done on live programming already. Yeah, yeah. So I really love that part of your work that you have not only the static abstract code, but like live data.

How will that... But I missed like the significance of how that would be interesting in the context of a palette. So the purpose of like the GUI is basically to give you kind of... For many palettes, the purpose of the palette is to give you a preview or something

of what that value is eventually going to do when it's run mm-hmm yep so when you're constructing the plot it's sort of meant to be a preview of what the plot will look like when you run the program to produce the plot what if we didn't have that gap there right what if we could just show you the data you're plotting as you're constructing the plot parameters and so on and and that's why it's really useful to have that live information and to run run the program before it's done it's like before the pallets even kind of before you're done interacting with the pallet you could still run the program and get the information that the pallet needs to give you even better assistance i see cool so i think there's lots of examples of like

monitors and things that you could basically do where you basically put in a palette whose only purpose is to show you the value of some argument that you provided to that palette in in line inside your program just for the feedback like just for the feedback like the code it generates might even just be like unit sometimes cool yeah or like it takes the argument and gives it back to you as the identity like it behaves as the identity function, but its display gives you information. I feel like that's kind of like equivalent to console.log. And like if the behavior you want is, you know, just show me the value of this thing,

I imagine there should be like an editor magic that does that without having to, you know. Yeah, if it's just literally show me the value of this thing, maybe that's not what you want. But it could be like show me some, you know, some particular way of displaying this type of thing. Yeah, that makes sense. Where you want some control over that. Yeah. yeah that makes sense where you want some control over that yeah um so one quote that i i think i pulled out of one of your papers was um you talked about recasting tricky language mechanisms um as editor mechanisms oh yeah um

yeah so there's this whole host of language mechanisms that are used basically for convenience. So what's a good example? Import star, right? It's really terrible to do import star because you've just dumped the entire set of bindings from this library, which might change into your scope and code evolution is really difficult because things start shadowing each other and so on and the only purpose of import star is because you're too lazy to like explicitly qualify everything uh as a programmer

and that's totally legitimate right like that's the kind of laziness that we, you know, like eating your porridge, right? Like it'd be nice if we just could eat what we wanted, right? But not get the bad side effects. So you can imagine import star just being an editor directive that says, I want you to hide the fully qualified, like I want you to suggest to me things from this library and hide their fully qualified names in the visual display. But in the actual code, everything remains fully qualified. So there's no worries about library evolution and things shadowing each other and not knowing what's in scope and so on.

So that's one example. Another is there's this whole set of language mechanisms around implicit parameter passing. So type classes are actually really just implicitly you're passing these dictionaries around to not have to explicitly pass around the equality function for every type that you use equality on and so on. Scala has this whole very complicated implicits mechanism. OCaml is developing an implicit modular implicit which is a way of passing first class modules around implicitly for many of the same purposes as in Asclone Scala.

It could be, and I'm not sure if this is the way to do it, but it could be that since the purpose of this is literally just convenience, you don't want to pass these things around explicitly, what if that implicitness was just part of the editor where like things are being hidden, things are being passed automatically unless you override them, but the semantic model of the language doesn't have any of the simplicits in it. It's just still the very, you know, very easy to reason about semantic model of, say, ML. Right?

Yeah, that's a fascinating idea. Yeah. So I think there, yeah. Well, i don't know if it'll work but it's something to think about at least and having this co-design that you're doing where you're designing a language together with the editor and you know you're going to have an editor capable of passing implicit things around really allows you to just be like no we're not going to worry about that in the language design that's for the editor side so i wonder what you lose if type classes are now implicit um like it feels like i could be wrong but to me it feels like uh type classes and haskell are this

this almost like a tool to reason about and they have certain laws they're like yeah they're more than just the sum of their parts somehow and i worry if like the if um the the language doesn't actually talk about these things then maybe the editor will be forced to do these eclipse like heuristics to like you know map backwards to type classes when you could have just put them in the semantics? Yeah, so type classes are really just kind of an impoverished module system in a lot of ways. They bundle together a bunch of functions and these laws are like relationships that should hold about those functions

together with a single type that they're talking about or sometimes multiple arguments to these side classes. There's a mechanism in OCaml called modular that's being developed in OCaml called modular implicits and it's based on this paper called modular type classes which separates that those two aspects of type classes so the implicit passing of things is one part of the type class mechanism and that sort of bundling functions together to talk about a type that's sort of an abstract type is another aspect of type classes and interesting those two things don't need to go together okay and the thing that I was worried about losing is the abstract bundle. Yeah.

Yeah. You were worried about losing the module system aspects of it. And I think those things come from having a proper module system, which the Haskell world has sort of slowly started to realize they need a module system. And there's this project called backpack, backpack, which tries to back patch a module system into the ASCLE build system, basically.

It seems like an interesting approach. It seems like it'll work out, but it's a lot nicer to have it be actually a part of the language than at the level of only package management. Yeah, got it. So with Hazel, we want a proper module, ML-style module system at some point. The development of Hazel is very rate-limited by just how much time the few of us that understand that code base really well have to work on these things. So it might be a little while before we get a proper module system, but we want one.

I see. And I guess, I don't know if you're the right person to ask this question too, but as far as the type classes laws go, are there any programming language semantics that have laws embedded in the language itself or without like only be like a language like cock or something yeah I mean when

you start talking about the equational behavior of functions you need a type system that has support for reasoning about equational behavior and then you're doing it independently type programming there are refinement type systems that have sort of refinement type systems are kind of in between in certain sense sort of simple type systems and dependent type systems where you can say like this

is an int such that you know X is an int such that x greater than zero. And then you've defined this predicate on values of that type int. And there are ways to, there's some really cool work in Liquid Haskell on kind of encoding the equational proofs into refinement type systems, which are actually simpler in some ways than full dependent types. This is work by Nikki Vazow and Ranjit Jhala and some other folks. But yeah, it's difficult to actually, yeah, Liquid Haskell the thing i would that would maybe answer your question if you want to stop short of full dependent types but still reason about type

class laws got it yeah yeah a lot of people pushed me to liquid haskell and dependent types and refinement types so i probably should actually learn what these words mean at some point. Yeah, I mean so like verification of these like non-trivial program properties is another really interesting research area that's been a lot of what PL research has been about for many years. So yeah I find that like that's another thing that we haven't done much with in Hazel yet, but, like, editor integration of these kinds of things where it, like, helps you discover the invariance and then prove them correct and prove your code correct. That's, like, another kind of frontier of PL research that has a lot of foundational research already done, and it needs to kind of be put into practice it's inside an editor so um so speaking of foundational pl research i think now is maybe a good time to um ask you to defend it because i think there are a lot of people i i don't know if if uh again you're the best person to defend it, but I think you're particularly credible to my audience because you're someone who's clearly concerned about the programming experience and improving the lives of programmers.

So I don't think someone listening to you would think, oh, well, this guy is just like an academic who's just proving abstract properties of things nobody cares about. And yet, it seems like you really think that the mainstream programming languages, research, Greek letters stuff is providing value. When I think a lot of us, even smart people, look at those papers and just see esotericness. Like I recently, you and I interacted on Twitter where Eliezer Yudkowsky, a very smart programmer, and Paul Graham, also another very smart programmer, were bashing Greek letters and the new computer science paper, like what new computer science papers look like. So anyways, what's your defense?

Yeah, there's a lot there. Um, there's a lot of different views on, on Greek letters and math and its value. I mean, if you step away from CS, if you told a physicist that math is superfluous, you get laughed out of the room right like you can't do physics without math and as you get more towards the sort of human sciences people become more and more hesitant to involve math and I'm not sure that really makes sense right like obviously there are other things you have to involve when you start talking about designing things for humans it's not strictly math but there are many many just mathematical questions at the heart of programming language design and if you try to do it in any other way you you're just flailing in the dark right so um

well so i think just i was going to say um i feel like part of the like the quick counter argument to that is there are a lot of people who make a lot of progress you know make billion dollar businesses or whatever doing programming and not and not doing the math stuff they are doing math i mean they're just doing math kind of by the seat of their pants right and they don't ever feel that they don't feel that confidence that you get from knowing what you're doing. There's a lot of reasoning by analogy instead of reasoning from first principles in programming as it's typically practiced, where you go on Stack Overflow

and you find some code that's kind of vaguely similar to what you think you need, and you copy it in and you see if it works. And you fiddle with it if it doesn't. And yeah, that's fine you can you can build you know you can build bridges without understanding calculus that doesn't mean you can build the golden gate bridge without understanding calculus and as we start solving more complicated problems in computing we're going to need more mathematical rigor and discipline than we needed to build apps and things for limited purposes.

Then the other question is, yeah. Okay, so I think math is really valuable. I think it's very intimidating, especially when you start using letters that I remember when I first started reading PL papers, I didn't even know what the letter was. I didn't know whatever taught me the Greek alphabet. So you're not in a frat? Right, I mean, that's the only background I had.

I wasn't in a frat, but I went to University of Illinois for undergrad, which has a very large Greek system. But yeah, that was the only way I really knew what some of the capital Greek letters were. But there's a lot of lowercase Greek letters in math, too. So, yeah, I think that's really a failure of training, right? Like I think you can get a computer science degree without anyone ever even attempting to teach you how to do this stuff because there's some assumption that it's too hard or you won't need it.

And so it's just a circular kind of situation where no one ever learns how to read the papers that we're writing. And so they are very difficult to read if no one's ever taught you how to read the papers that we're writing and so they are very difficult to read if no one's ever taught you how to read them but and there's also this failure of expectations right if you if you see 10 pages or five pages of of a paper then you have your brain sort of has this expectation for how long five pages takes to read. And that expectation will be grossly and frustratingly violated if you try to read a five or ten page mathematically dense paper

in the same amount of time it takes you to read ten pages of a novel. That's well said. But you shouldn't come in with that expectation, right? You should think of math, mathematical notation as a sort of compression scheme for knowledge. And when you first start reading math in a domain, you're going to have to completely decompress it. And that 10 page paper will be like 100 hundred pages decompressed or more. Right. Like, I don't know what the compression ratio is for type theory, but it's pretty high.

But what's, what's great is once you've started doing that decompression long enough, it happens in the sort of subconscious. And then you can read these things very quickly because your whole brain is engaged in processing them instead of just the sort of frontal lobe that's manually decompressing them and trying to understand what's going on. And so after some amount of time, it becomes really valuable to have mathematical notation. If you look back at the history of mathematical notation, which is very interesting, like Euclid's Elements, which is like 3,000 years old or something like that, it's this text on geometry, and it has some geometrical figures, and then it has text written in Greek longhand. There's no symbols, except occasionally a symbol referring to an edge of some geometric figure or something like that.

And so these pages are just super tedious to read. Like you have just full sentences that are like, you know, add this to this and then square it. And those are all just words on the page. But this is what math was for a long time, I think, because yeah, like it wasn't obvious that there was this other way to do it that would be like initially a little imposing, I think, because yeah, like it wasn't obvious that there was this other way to do it that would be like initially a little imposing, but eventually much nicer. It wasn't

really until even like the 1600s when the printing press and all these things started democratizing learning about these topics that people said, do we really need a print this much to convey this idea? Can we actually abbreviate some of these things? And so you started with abbreviations of and, which became plus. And slowly more and more abbreviations started entering. It wasn't matrix notation. It's like late 1800s and Leibniz and had some calculus notation that's persisted, which I don't actually think is very good. And it's really only in the 20th century where like math exploded and became a part of everything.

That notation also exploded. But in every other domain, we don't expect, you know, civil engineers to understand calculus without taking three semesters or more of it. I think we need that same expectation for like, like learn how to program without the math, of course, right? Like use Stack Overflow, write cool stuff. But also slowly, whether or not you're in college, whether or not it's immediately relevant to you, like read a little bit more of the theory with the expectation that it's going to take a while and it's a long-term learning process.

And then you end up in a place where it's just very, you can understand complex concepts very quickly and very precisely. And you feel this keep using the word confidence like i feel confident about my understanding of something like polymorphism because i've studied the theory of it in a way that just like using polymorphism in practice a lot maybe wouldn't have made me as confident in what i'm doing yeah well i think that's that's quite a good pitch for studying math so

would you have some concrete um places to start learning like yeah we already mentioned tapple and um bob harper's book what are the other yeah those are those are great starting points you don't need to even read the whole book right like i think the first quarter of the book is enough to then like pick up as many PL papers and start to understand them. Um, I do wish we had more, like I was saying at the beginning, you know, I wish we had more, um, surveys and introductory material and places where you take all the contributions that exist in papers and bring them together, this sort of wiki idea. And so I hope one day to, you know, be involved in building such a thing. But for now, textbooks are great. You know, this Twitter conversation you mentioned, I think one aspect of, I don't remember who

said it, but one of the people in that conversation said basically like introductions in papers aren't written for, you know, for everyone anymore. And that's true, right? Like there are page limits. And when I write a paper, I'm writing it for the audience of that conference, which is not the general CS public even. But the reason for that is I can build on these very nice textbooks that exist, right?

Like my papers are written for people that have read the first quarter of those textbooks. I'm not going to try to re, you know, rewrite those textbooks in the interest section of every paper that I write. That would be a colossal waste of time and space. Well, yeah, that's a a that's actually an interesting like I have an interesting lens on that way that thought because um uh I spent a few weeks ago I spent a long time on on a like an introductory paper to like a very dense mathematical topic and i tried to write it for a general audience and it did not go well yeah and i think part of the issue was i was writing

about a complicated subject but with the tone of like you'll be able to get this if you just read my writing yeah and and i think and i now i kind of wish uh uh like i was i'm considering putting at the top of the article. Like if you don't already understand these concepts, don't read this article. Um, yeah, that would be great. I wish we had more of that. Like, here's the, here are the prereqs for this paper. Please make sure you at least look briefly at these things first.

Yeah. Well, cause it's crazy. Like when I go to install a piece of software and then they're like, they don't list the prereqs, what I need installed for. Like I just, I hit, I hit install and they're they're like oh like it just gives me an error like this thing isn't installed it's like what like how could you not list it to prereq yeah yeah yeah i mean somehow this is a very difficult problem in computing right dependencies yeah different software has with other software yeah well well so i guess what i was getting to is that greek letters

or like certain things like that kind of do that by proxy it's like if this scares you like you'll just stay away on your own you don't need the like warning sign yeah maybe but there's i mean greek letters are used in all sorts of different domains right there's basic type theory that uses greek letters but there's like other there's papers written where you just need to have read other papers in that field and there is no textbook and there's no survey paper and I think that's a shame but that's that's still true and those are the papers where I think you really need this kind of like guide to at least point you towards the right papers. Sometimes a good intro should point you to the right things to read to understand the rest of the paper.

Yeah. Yeah. So thank you for your defense of theory. Oh, well, actually, there was one other thing that I wanted to tee up for you because I remember when we were in Boston together, I, I asked, I forget what it was that I asked you, but I, I, I mentioned something about like why you're working on theory. Like it was a similar question of like defend, defend your, your profession, defend theory. And your response was like,

like theory has this generality that like it might not work with the tools of today and the fads of today. Like theory has this, like it'll be around for forever and it'll be applicable in many different domains. Yeah, exactly. So it might be that it might be that people end up using Hazel itself. I'm optimistic. But regardless of whether that's true, the papers that we're writing with theory in them are relevant to anyone in the future who has these ideas about structure editing and liveness and so on. And the future is a very big place compared to the past of programming so far or even the past of mathematics so far hopefully right hopefully humanity survives and uh it seems inevitable that at some point

someone else will want to develop a structure editor like it would be very uh it would be i would need a lot more confidence that i have than i have about the future of hazel to just be like i don't need to talk about what's going on people will just use hazel i need to do it once and that's it right and so the generality aspect is just the future is much longer than the past so we should be writing for the future well then it's almost like why waste your time building hazel because it's just one shot in the dark and and they're an infinity there's an army of people in the future who might build things why don't you know but there's lots of there's lots of theoretical questions that will come up as hazel develops further and we'll write and we'll write papers

about those those things that will be relevant to people in the future that come up on the same problems i don't want to understate i like i do want i think we're in a very uh important part of history here at the beginning of computing um where the choices that we make now will resonate over hundreds of years potentially. And so I'm not completely just leaving the future to the future, right? But in the case that we don't solve all the problems in my lifetime, I do hope that the things that we develop now will be built upon in the future and not just reinvented constantly and poorly. Yeah, yeah. It's almost like a backup plan worst case scenario um yeah because i guess if you just

um wrote your insights into code nobody's going to go back and parse them out of the code and and put them into the next their next thing, so that code is math in my mind. It's just, like, if you think 10 pages of Greek letters is hard to read, try reading 40,000 lines of poorly structured Haskell instead. Right? Like, that will take you a lot more time than it takes you to read 10 chapters of a textbook and then 12 pages or like two pages worth two papers worth of hazel stuff uh so hazel's written on camel so yeah hazel's about you know right now hazel's very austere but it's still about 25 000 lines of code

the implementation that's going to take you a lot longer to read than our 25 pages of paper and yeah be a lot harder for you to get the essential ideas out of that code base then it's gonna be to get them out of my papers hopefully so hopefully yeah I think that's a pretty good pitch. Math is compression, what you said before. So I'm realizing now that there was one topic of Hazel that I left out that I want to come back around to. Collaboration and how this edit semantics you have could be extended to have like multiple people editing the same code base at the same time. Yeah. Yeah, that's something i'm really excited about um yeah right now we have this edit action semantics which tells you what edit actions do but they all assume a single cursor and

of course oh so the cursor is part of the edit semantics. It's like formally represented. Like when your cursor is here. Oh, interesting. Yeah. That isn't obvious to me that like, because I would almost think of having edit semantics. That's like a bird's eye view semantics. Yeah, there's other ways to represent.

I mean, there's some other ways to represent where the cursor is than we choose. I think you want a cursor or multiple cursors. I mean, you don't want the edit actions to just be, they need a locus of action. Your edits are happening somewhere. That's what a cursor gives you. Well, I guess now that obviously makes sense based on the way that we edit code now and text editing. But now that I'm wondering if, I don't know, if you could rethink it in a way where that

wouldn't be what you want. But I guess you're right. You do want a locus of action. So a cursor makes sense. Yeah. It's hard to imagine doing just like transformations on the whole program from the top without referring to a place in the program. There are different ways to refer to a place in a program. You could have unique IDs for AST nodes and refer to them that way.

But then like the selected unique ID is effectively the way you're representing the cursor. So it's it's um isomorphic in that way okay but with uh yeah so with uh collaborative editing right you want to have multiple one way to put it is you want to have multiple cursors another way to put it is you want to have multiple replicas of uh of the editor state where maybe in each replica there's one cursor like each person has their own replica and their own cursor in it but then you want some way for the so yeah so in each replica you're editing it by creating this history of edit actions that's that's changing the code and you can represent that change by you know a structural diff but really but really the things that cause that change

are the edit actions that you performed on that replica. And so what we want to do is have some semantics for edit actions such that you can interleave these edit action sequences from different replicas and leave the program in a consistent state for all the people viewing it. So this subsumes collaborative editing in the Google Docs sense and it also subsumes version control in the Git sense because all of these things are just you have different people performing edit

actions on replicas and then you want some way to combine them and the way we can combine things right now is these structural diffs which often obscure what you actually did because it needs to be evident with just kind of without any like notion of history so what if we represented change instead of instead of with structural diffs? You represent change with sequences of edit actions, and then you have a semantics of edit actions that has this theoretical property, right, that you figure out using Greek, that says that there's a convergence right if you merge these replicas used by merging the sequence interleaving the sequences of edit actions you get an equivalent output for some notion of equivalence now to make that work you need some notion of conflict in your semantics as well so the

simplest example is you just have two replicas. They each have a hole in it. One person fills that hole with three, and one fills it with four. There's no way to create a consistent view of the edits that happen to those two replicas by choosing three arbitrarily or choosing four arbitrarily, right? Yeah. You want to somehow represent conflict and put the three and the four there and say, well, everyone now consistently sees that this is a conflict and then there are some added actions available to resolve conflicts and those go through the same process.

And so it's kind of like, you know, when Git inserts these like less than, less than, less than, less than things, except the editor understands them instead of it just barfing because it's not part of the programming language syntax. Yeah, I like this theme. It seems like you're reifying errors into the programming language semantics. Now you're also reifying conflicts into the semantics. Yeah, exactly. Very cool. So you're taking almost all of the auxiliary tools in programming

and you're putting them into the semantics of the language itself. Yeah, yeah. There's this danger of trying to reinvent everything, which is just a lot to bite off, especially as a researcher. But I think this is a pretty natural thing to start thinking about when you develop a structure editor is how does change get represented? And yeah, and what this is all related to is this notion from distributed data structures called the CRDT, which stands for conflict-free or sometimes convergent replicated data structure. So there is theory, you know, there's some nice

papers starting about in 2011 on CRDTs for much simpler data structures like, you know, sets, right? Like an insert only set. It doesn't matter matter what order the insertions come in, you just can replay them in any arbitrary order and you'll get the same set. And so what if instead of the data structure being something very simple like a set, what if it was an expression, a typed expression in the lambda calculus or in some extension of the lambda calculus? So that's kind of the research question there is can you make a crdt for this very semantically rich data structure yeah that does sound like a hard question and to your point of it's like worrying to reinvent everything about programming yes i i see that that's a worrying thing for just you to do by yourself

But I do like the idea of reinventing everything that has to do with programming That's kind of now on the side It should have been ad hoc, seat of the pants Well, this language doesn't do this thing, so let's put it in the editor I really like the idea of taking all those things and putting them into the into semantics uh like so we have like mathematical confidence about these things and and to the point that you said earlier um we we also have the ability with these greek letters to test out some of these things independently so it's not like you cyrus have to

do all of these things but it's almost like yeah it they're all a lot of them are orthogonal once once we've as a community kind of agreed upon the fact that okay we're going in the structured editor direction and where um we care about programming experience and we care about like embedding everything about programming into mathematical semantics then all of a sudden like researchers can be freed up to work on like you know someone else can work on the collaborative the crdt problem and you don't have to you know you don't have to worry but when they're done you can just kind of import their their greek letters into your your code base yeah yeah i think yeah this is kind of an underappreciated benefit of having a thing

like the lambda calculus is like in many ways it's the most widely used programming language in in computer science research right because so many researchers build on the lambda calculus much more than there are researchers that build on any particular programming language uh and they can all that work is going towards this kind of common vision that's emerging um where yeah like one person can work on what collaborative editing looks like with the lambda calculus and one person can work on what live programming looks like with the lambda calculus and those things are very easy to merge because they're both based on the lambda calculus as opposed to if like one person did it with OCaml and one person did it with JavaScript, it's like, okay, now we have this third problem of how do we make

this all make sense together? So there's like, there are a few things, but one in particular idea I've had for improving programming that I, not until this conversation did i think like oh maybe i should prototype this um like on top of the lambda calculus instead of you know like in a broader you know seat of the pants experiment you know yeah um so it and maybe And maybe they'll just point me to literature where this already exists. Hash, where the terms in a programming language are referred to by the hash of their definition. Uh-huh. Yeah, that idea exists. I don't know of anyone that's done that with the lambda calculus, but I haven't searched for that.

Because to me, does the lambda calculus have definitions? Or it doesn't have, like... It doesn't have definitions in the sense of type definitions or module definitions or anything like that. There's no sense of labels. Yeah. That's what I'm wondering. This feels like a label-y thing. But you can label.

I think there is something called the labeled lambda calculus, where each term has a unique label on it. I'd have to go look at that again to remember what the purpose of that was. DAN GALPIN- Well, I guess maybe the broader question is, are there some times when simply type, or some lambda calculus isn't the right medium for programming language experimentation, where you'd say, you know

what, you should just whip out some code and experiment with that by the seat of your pants. I'm not opposed. I write code in the context of experimentation sometimes before I do lambda calculus-y stuff. Wow. So risque. I'm not opposed to that. i don't do it that often

actually i do mostly start on paper with the lambda calculus to be honest but um uh definitely user like you know i work on the kind of underlying mechanisms the semantics for the live programming and all this stuff there's a bunch of ui stuff that i yeah i'm i don't focus on and when i do do ui stuff for hazel i just implement it and play with it and see how it works right there's not a lot of ways to do math ui stuff yeah yeah yeah so like if it is a ui experiment that you're doing by all means do a ui experiment with code um or all right well said with other with other methods like mock-ups we did some mock-up stuff in that xe paper we were talking about um as far as yeah well i guess part of the question um you're talking about like content addressable kind of yeah well encodings right well yeah but, and part of why I was inspired to ask this question

is before this conversation, I never thought of like Git, which seems very much like orthogonal to editing, orthogonal to like the semantics of a language. Like the semantics of a language, I thought was about like, you know, how to evaluate the language. And all of a sudden you're like,

no, actually, like if we haven't edit semantics, now all of a sudden, like Git has like like if we have an edit semantics now all of a sudden like git has like formal semantics like look at that yeah yeah edit actions they submit having a semantics for edit actions is so beautiful right it gives you this way to talk about change and programming and all this stuff that we've just thought about informally like if you think about it like we if i asked you or if i showed you three plus four plus and then i stopped there and i asked you tell me what's going to happen here you as a human very easily as you're going to say it's going to be seven plus whatever you're going to write yeah but until very recently we had no way to say that formally. And it's the same way with edit actions.

Like we have this very rich mental model in our mind of what editing means, but there's no way to talk about it. And now we have a way to talk about it in, in mathematics. And so, yeah, I think it opens up a lot of interesting research directions that I'm really excited to work on over the coming years collaborative editing is one of them so um I I usually when I see in your presentations you when you talk about collaborative editing the next place you go is also very exciting to me you talk about this computational Wikipedia yeah yeah well we started with that almost yeah well so that was almost

like a scientific wikipedia and then well actually and you're right computational in that well and it depends what you mean by computational because i think maybe the weakest way to interpret computational wikipedia is it's wikipedia but there's a place where you can press a button and they'll run some code and give you the results and it's like wikipedia but it's like also jupiter notebook and i think that's like whatever like it's kind of cool yeah it's like wikipedia but it's like also jupiter notebook and i think that's like whatever like it's kind of cool yeah it's like not only can you embed pictures uh you can also embed code right but i think that would be useful but that's not exactly what i have in mind i have

something kind of grander in mind yeah i think one of the things you said about it that stuck with me is what if we i don't know if it's what you meant if you imagine all of software as being somehow connected and it's like one single all the different software is just one single piece of software and it's all being edited to collaborate at the same time and yet like when one person's in the middle of an edit not everyone else's computer is crashing right yeah so imagine yeah imagine something the size of wikipedia or the size of the internet, right? Which is actually formally a single mathematical expression. It's just massive expression.

And it's evolving through this edit action semantics and people are running bits and pieces of it because you can run bits and pieces of stuff now that we have this semantics for incomplete programs. And yeah, so one person editing one page and stopping in the middle of what they're doing and getting some coffee won't. If that brought down Wikipedia, this would be completely infeasible. But solving the gap problem, really solving it where there's no gaps, allows us to

really think about this in this very elegant unifying way that's rooted in thousands of years of history of mathematics um so you know i think that's a nice thought experiment could we actually have a mathematical expression that big being edited by many many people and have it serve the same purposes that like separate siloed programs and pages and things serve today i think so i think there's lots of technical implementation questions that would arise at that scale i don't know how fast my code would run at that scale but uh conceptually i think it's doable yeah i i it's funny you and i are i guess are quite similar in that my vision for the future of software is also quite similar in that um like a single expression can represent this really rich, complicated, gooey,

you know, can represent like all of software basically. Yeah. I don't think I personally thought of putting all of software in the same expression. But it's the same. I think of it as like the same medium. Basically, like on GitHub, how you have different projects. Yeah. To me, those boundaries always felt kind of artificial

yeah when I say this sometimes people ask me about versioning if someone's editing a library that you rely on it's going to break your code this could be chaos and you know

there's ways to solve that by pinning things to different versions and all this kind of stuff but i kind of want to just like embrace the chaos of it uh i just i want i want like my code to break because someone else is editing another page on wikipedia and then i want them to come over and and and help me fix my code and i want to go over there and like watch them as they're coding and see what changes that they're making and ask them about it and keep everything in a single consistent state instead of trying to pin things to different versions and oh that's interesting yeah like i know you can do that and then you know in other settings that might those mechanisms might be necessary but for for something like Wikipedia, just embracing this,

just the life that this artifact has, I think is something that I'm really interested in. Huh? Yeah. Yeah. I like, I like that sentiment, even just to push us to like, think about, you know, what would have to be true in order for that to be viable. Yeah. Because I think you could look at Google Docs as doing that. It totally embraces just... And the reason Google Docs is able to do that

is because it solved the gap problem. There's no point at which Google Doc will break. And so because you've solved the gap problem, just because I'm working on paragraph one and you're working on paragraph seven, but in code, like there's nothing you could do in paragraph seven that's going to really screw with paragraph one too badly. So in theory, once the gap problem is solved, potentially maybe a lot of the issues in terms of why we fork code and version code go away. Yeah, I think so. I mean, some of the issues won't,

like you need good refactoring tools, right? You wanna say if I change this type definition, add a new case, then I want to offer that refactoring where all the pattern matching on that data type now has the new case and maybe there's a default or something right like that yep doing that with without good refactoring tools is probably gonna annoy people but there's another set of research problems is how do you make good refactoring tools in that setting well i think

that that's part of what i like about your sentiment instead of saying like oh well you know any refactoring is going to be messy so let's just like like uh pin things to versions because that you know it's all a problem instead of that let's um like challenge ourselves to make refactorings so good that um we don't need to pin things to versions like the things things will somehow just evolve beautifully over time if you give people the right tools i don't want to say it's going to be beautiful. I think there will be chaos. Like that's why I use the word chaos.

I think sometimes it'll be like annoying, but that's okay. It'll be beautiful. Sort of the whole thing together will be beautiful, even if pieces of it are sometimes annoying. Cool. So before we sign off, I wanted to, um, get it. I wanted to hear an update of, uh, your academic life and how, cause I know, I think the last time we talked, you're looking, you were looking, implying the

jobs as like a professor, assistant professor. Well, I guess I just want to contextualize. People who listen to this podcast are interested in programming, computer science and the future of programming. And I think a lot of us go about it at different ways. And so I think there are a lot of us who are interested in the academic route, but don't have a lot of insight into it. So yeah, if you could tell us where in the process you are

and how it's going that'd be great sure um yeah so i'm looking for tenure track faculty positions as an assistant professor uh primarily i'm really i mean i'm looking for a place where i can do this kind of work right where i can when a theoretical question comes up i work out the theory and i also get the opportunity to work on these kind of long-term visions and these experimental platforms that maybe aren't immediately useful and uh academia is one of the few places where that kind of thing is at least nominally supported. Um, and yeah, um, you know, I applied to 54 places, right. Just all over the place where that's yeah.

Uh, like, was this like you just checked 54 boxes and hit apply or you had to actually do 54 applications you so to submit yeah so it's a lot of the material is the same right you write a research statement that's kind of three or four pages about what um research you've done and what you plan to do in the future and why it's important and interesting and uh and then you write a teaching statement which is yeah summary of what you've done with teaching and what you plan to do, what kind of classes you want to teach, what your teaching philosophy is, what your advising philosophy is, that kind of thing. And a few places have a diversity statement now where you talk about ways you're working to broaden participation in computing and in research. And then you write a cover letter for each place.

That's kind of, you know, the form of the cover letter is the same for each place, but you say something specific about each place. And so each application took between 10 and 30 minutes individually to write that cover letter basically. And to do the research. Um, so it was a lot of work in writing the research statement.

I mean, it's three or four pages, but it takes some, as you know, it took as much time as writing kind of a full paper did for me because you have to put a lot into those pages. so it was, yeah,

it was a couple of months. Basically it made, that was my main project was applying to these jobs. Um, and, uh, yeah, it was a couple of months, basically. That was my main project was applying to these jobs. And yeah, those applications were due kind of in December. I'm starting to hear back from some places now about getting some phone interviews and a couple of in-person interviews. It's a pretty stressful process um different departments have uh different areas in cs that they're really focused on a lot of things nowadays are very focused on ai and machine learning and um cyber security is a big thing and there's all these you know like

funding things that you have to now start thinking about like who's going to fund the work and yeah so it's uh you know it's very much like a lot of people make an analogy between being an assistant professor and like starting a startup you're recruiting and you're raising money and you're trying to convince people like old people that maybe don't really get what's going on nowadays that well that you're exciting and and you're not doing work that's been done in the 80s as you know like someone who works on structure editors a lot of senior faculty are like oh yeah i remember the cornell program synthesizer in 1982 and i'm like okay well i read about that as well and i think we're doing some new things but you know you have to convince them that you're not just unaware of and retreading work that's been done in the past that

um it's already finished so it's yeah it's really on it's unclear you're writing these things for people you don't know you don't know who's gonna read them you don't know how they're gonna respond so it's pretty stressful um but the goal i mean the the yeah if all goes well i'll be in a good situation i think where i can work on these kinds of ideas without having to um having to think too much about quarter to quarter stuff right the way you have to in most companies yeah um that's that's the real benefit of doing it in academia that and the colleagues that you have right you have people that very smart read the papers you know could point you to uh papers that are relevant to you that can talk to you in terms like that. They have all read the textbooks, right? They can talk to them in Greek on the whiteboard.

And so, yeah, it's definitely not for people that are interested in life and in the future of coding. It's definitely worth considering like going to grad school. It's not the only way to do it. And I know there's a lot of people that are managing to like kind of do this work on their own like you and a lot of other people in the live community um but it is you know it's an option right there is support for this kind of work there's a lot of excitement you know i go i write papers about this kind of stuff that we're talking about to

conferences like Popple, which are very much just like theory conferences. And there's a ton of excitement there. You know, people are really happy that someone's bringing these problems to them in ways that they using tools that they've developed. So it's not, you know, it's not like I'm being antagonized for working on these kind of user facing problems. It's, I feel supported by the research community. Well, that's great. That's awesome. Um, cool.

So let's, um, finish up with the final question. Um, more logistical than anything else. Uh, where are the places on the internet, uh, that people can interact with you? And in which ways are you looking for people to interact with you sure um so you can read more about hazel at hazel.org that's my main project right now you can find me on twitter my twitter name is neurocy and e-u-r-o-c-y and uh i'm reasonably active on there unless you know i had a new year's resolution to be less active on twitter so i'm less active on twitter now it's funny to like

i wonder what it's like to start a company where people's new year's resolution is to do yeah use less of your product yeah exactly if hazel's not in that camp one day i might call this the waste time on hazel less um well i don't know if anyone's like i really just gotta spend less time on wikipedia it's just it's just too much of my time i've had that thought i remember like procrastinating on studying for tests and college and on wikipedia so maybe it'll be like that um and if you're interested so if you're if you're interested in hazel and getting involved in the hazel project we're definitely open to that we have a slack channel uh that i'm happy to invite people to um It's got about 50 people in it right now, so it's kind of, it's a lively place. And yeah, there's a bit of a, you know, we've been talking about like,

yeah, there's a bit of a initial effort that you have to put in to learn a little bit of theory and to read the papers that underlie our implementation and learn a little bit of OCaml if you haven't learned that yet. But we're happy to support people doing that, asking questions as they read these things, trying to figure out what's going on. So if that's something you're interested in, definitely send me a message on Twitter or send me an email. You can find me on Google. I have a webpage.

That's very generous. That sounds like a really... That's very generous. Yeah, I think it's a nice, you know, I acknowledge that theory has been unapproachable for a long time, and I'm trying to do what I can to make it approachable. And one of these things is like, I'm very open to this mentorship kind of thing in this, in the Hazel Slack and in other ways. Yeah.

Cool. All right. Well, um, thanks so much for your time. This was a lot of fun. Yeah, this was great. I really enjoy your podcast in general. Um, really thanks for, thanks for, this is like a great service to our community I think. Oh, wow. Thank you. Um, thanks for listening. I, I'm glad it appeals even to someone as uh seriously great as you i don't want to like i want to get away from that like oh you're elite

because you know greek right like like let's democratize greek greece was known for its democracy right well said well said all righty All right, yeah, thanks, Steve. Thank you. If you enjoy these conversations, I bet you'd fit right into our online community. You can join our Slack group at futureofcoding.org slash Slack, where we chat about these topics, share links, feedback, and organize in-person meetups in various cities,

New York, London, now San Francisco, Boston, and also Kitchener, Waterloo, and Canada. If you'd like to support these efforts, there are a few ways you can be helpful. I would really appreciate any reviews you could leave for the podcast, wherever it is that you listen. If any episode in particular speaks to you, I would encourage you to share it with your friends or on social media. Please tag me if you're sharing it on Twitter at Steve Krause so I can join the conversation. I also accept support directly on Patreon at patreon.com slash Steve Krause. And as always, I am so thankful for the ultimate form of support, your constructive criticism. So please don't be shy with your advice.