#39 - Mathematical Foundations for the Activity of Programming: Cyrus Omar

06/07/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 an incoming computer science professor at the University of Michigan bridging these disciplines by creating the foundations to precisely reason about the experience of programming.

Cyrus noticed that nearly all PL research focused on the semantics of complete programs, while programmers spent almost all of their time in between states of valid programs, editing and iterating towards their eventual vision. In order to understand these incomplete states, Cyrus has done theoretical work on typed holes, which can be empty or filled with something of a mismatching type. Cyrus compares this idea, which is similar to holes in Haskell and empty fragments in projectional editors like Lamdu, to the mathematical concept of zero: the importantance of explicitly modeling nothing. He built an extension to the lambda calculus, which he calls “Hazelnut”, which is what allows him to formally work with incomplete programs, i.e. programs with typed holes.

On top of Hazelnut, Cyrus built a projectional editor for his Hazel language, which he’s currently growing towards something equivalent to Elm. One of the most exciting early results of this approach is a comprehensive solution to the “gap problem”, which is when IDE services such as type a head go offline for a whole file in the presence of any syntax or type error. Hazel totally sidesteps this issue by automatically inserting holes where necessary to constantly maintain the program’s validity. This allows some for cool demos, such as evaluating an expression around an empty or filled hole and extremely localized type information.

We open the conversation with how Cyrus got his start in computational biology, but how his dissatisfaction with the tooling led him 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 than usual. Hope you enjoy as well!

Full Transcript

Transcript sponsored by Repl.it

Corrections to this transcript are much appreciated!

SK:

Welcome to the Future of Coding. This is Steve Krouse. 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 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 don't, who aren't considered programmers today. And I'm also really concerned relatedly to improving the programming experience, both of current programmers of today and also people who aren't programmers today but hopefully will be programmers tomorrow.

SK:

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 the ways in which I think programming can be improved and where we eventually want to end up with programming.

SK:

One person that comes to mind that shares that vision for what programming could be and how we can get there is Paul Chiusano who was an early guests 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 going to be right up your alley.

SK:

So, Cyrus Omar is currently a postdoc at U Chicago. He works with Ravi Chugh and Ravi's team. And before that, he was at CMU. And Cyrus has worked, 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.

SK:

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 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 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 this syntax error or whatever it is that you're doing.

SK:

And so, what Cyrus, his 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.

SK:

So before I bring you Cyrus, we have a quick message from our sponsor.

SK:

Repl.it 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 are 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 repl.it if you're interested in learning more.

SK:

And without any further ado, I bring you Cyrus Omar, welcome Cyrus.

CO:

Hi, thanks for having me.

SK:

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?

CO:

Yeah, I was into neuroscience. As an undergraduate and I started my PhD also in a computational neuroscience program. 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. I've always had a hobby interest in programming languages and tools. And so, I started doing side projects and those became my main projects. I was actually in the, I was in the woods for a summer, I was at Los Alamos National Lab doing like a research internship thing there. And Los Alamos is in this forest kind of up in the north of New Mexico up in that 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.

CO:

And so, it gave me a lot of time for self reflection. Yeah, I decided, you know, building tools to 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, 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. I was like, oh, this is an opportunity to be at a great place for this kind of thing. And so, I did it and it's been good.

SK:

Yeah. Wow. You're quite lucky to be at CMU by chance.

CO:

Yeah, basically. A lot of our lives are ruled by luck I think.

SK:

I think I felt like, I had a similar luck, I guess you could call it 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 work done by the Penn...

CO:

Penn has really awesome PL. We both lucked into being around fantastic PL people. Here we are.

SK:

There you go. And I guess potentially we wouldn't have done it if there weren't fantastic PL people around us subtly influencing us.

CO:

Yeah, probably not.

SK:

So speaking about tools, I saw one of your, it seemed like one of your earlier projects was like kind of an, it seemed to me maybe it was like inspirational for your current work. It was a project where you took like a regular IDE and then embedded like a regex playground and like also like the color picker widget inside of it. What was that project about?

CO:

Yeah, so that was actually the first project I did when I switched into PL. Yeah, it's called, the tool was called Graphite. It was this eclipse extension that basically allows you to use these graphical widgets to construct Java expressions. So those were two of the examples in the paper. There was like a color chooser that, 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 can 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.

CO:

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 an 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. 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 LaToza and Brad Myers, who are really great kind of empirical PL people. And so, most of the paper's 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 interesting set of design criteria, this sort of classification of examples.

CO:

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 kind of methodological paper, 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. 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, in 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 and Hazel.

SK:

Wouldn't that be funny if I decided not to ask you about Hazel in this conversation?

CO:

Yeah, we could just talk about my first project from 2012 for an hour. There's lots of talk about there. I mean, more generally, I think integrating 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, 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. So like Chrome or Microsoft Word or whatever. All of these offer you this set of primitives, which, 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. And so, I really want to take that idea and run with it and really merge the, return to the world where using a computer is programming a computer.

SK:

Yeah. I see that vision as well. I find that it's a very uncommon vision. Most people, yeah, like you said, think about programming as like the superficiality of what programming is. Like a person, probably like an Asian or white man or an Indian man with a Hoodie 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 text and anyone could, and more sorts of people can do it, all of a sudden, it stops being programming.

CO:

Right. It's interesting how that word 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. Now it's something that, you know, normal people use a computer, and those kinds of people that you described, they program a computer. I don't think that's right.

SK:

Yeah. So, I think that there is a true distinction between programming and using Word that like you want to help blur or get rid of that distinction. You want to like 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. In an earlier conversation I had on this podcast, I think it was Paul Chiusano who said that basically, it's just that the programming languages of Gmail or Microsoft word, are just bad programming languages and so we just have to make our user interfaces better programming languages. Would you say that how you see it too? Just adding stuff?

CO:

Yeah, in a lot of ways I think that's exactly right. Like if you analyze the set of actions available to you and where it is programming language, well, it's kind of an impoverished programming language, it's just some functions that you can call, but there's no abstraction mechanism, 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 texts 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 exists in mathematics in Word.

CO:

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 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, they're still those values then they can be manipulated programmatically. And then the key is really to be able to insert functions 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.

CO:

And so, that's how, I sort of envision Hazel actually eventually becoming an authoring environment where the programming environment, sort of conventional programming environment is part of its bigger kind of structure.

SK:

Like the programming environment's the base and you build an authoring environment on top of it, and it's always kind of, it's like a fluid transition from one to the other.

CO:

Yeah, exactly. The authoring aspects of it are just a mode of use of these palettes mechanisms which will allow you to manipulate certain data structures programmatically, or sorry, graphically, but underneath all of that, it is just values of various data types that you can also manipulate programmatically when the need arises.

SK:

Fascinating. So, I think the first time I came in contact with a vision of like an authoring environment, that was somehow more dynamic may have been Alan Kay's STEPS projects or basically any Smalltalk-y operating system world. Where did this vision come from for you?

CO:

I think I've read a lot about Alan Kay's stuff, so that's definitely part of it. The other part of it is just... I read a lot about... 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. You have this kind of just dead tree version of some piece of mathematics and you'd have to spend a long time implementing it to get it to work in your project. And so, I became very interested in sort of, in reimagining academia in some sense as contributing to something like Wikipedia collectively instead of contributing to this just like massive dead tree debris.

CO:

And I thought, well, what would it take to do that kind of thing? Well, there are lots of, especially as a computational neuroscience, I'd read lots of papers where there's 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 programmable sort of thing. And then, when I switched to CS... You know, CMU is a very type theory heavy school. And so the first class that I took as a grad student in CS was a type theory class, Bob Harper was teaching it.

CO:

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. I think it all just kind of flew... Like putting those trains of thought together kind of led to this idea. It took me a long time to get to the point where I could start thinking about it again. That paper, that Palettes 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. 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.

SK:

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've 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.

CO:

Yeah, exactly. I would say yeah, those are two of my top interest is for sure. I think there's still a very much a need for 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. I think having a place where 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.

SK:

Yeah, yeah, yeah. I feel similarly. I just want to point out one of the things you said there that I want... 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 like place. I too get the feeling that something about that's important. So why do you think that's so important?

CO:

I'm not sure that that's strictly necessary. 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 to deviate too far from that model, you better have a good reason.

SK:

I see.

CO:

But there's also a lot of excitement nowadays in not centralizing resources like that. And certainly, it takes a lot of money to run Wikipedia, right? And you have to donate to use it. So, it's not clear to me that it needs to be a single place. There's also different community standards, right? Like Wikipedia has a certain way that it runs its community and I know some people are not entirely happy with that. And it seems like its kind of premature to, you know, pick one set of rules for everybody. So, I definitely want whatever we build to be... For it to be possible for someone to run their own instance of this 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 people are collaboratively writing the encyclopedia of the computational world, which is increasingly the whole world.

SK:

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 just, you know, wear whatever clothes you want, you can do it. 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 scientific knowledge. Maybe this kind of a tool could be a workaround and get away from like Ivory tower of papers and all the artificial gatekeepers and somehow democratize science. Do you feel the same way about this medium?

CO:

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, I mean, in biology, you can do theoretical biology just with a computer. You can't really do experimental biology in your basement right now. There are some efforts to kind of do some stuff, some experimental biology kind of tool kits and stuff exists. But, it's really hard to imagine the kind of work that happens in neuroscience happening without institutional support. In some other areas in computer science, generally, 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.

CO:

But I still kind of struggle with that idea as kind of a way to do things like biology and chemistry, experimental physics and things like that. So, alternative funding models 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 in neuroscience. You have this place, the Allen 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. Yeah, that's the kind of thing I want to enable. But the conversation still needs to happen about how to like break free from the current institutions because they have billions of dollars going into labs and experiments.

SK:

Yeah, yeah. Well, I feel like the funding, maybe it's kind of like an orthogonal concern. It's obviously like deeply embedded... Anyways...

CO:

Yeah. The more it's an orthogonal concern, the better.

SK:

Yes, yes. Well said. So anyways, enough of us having fun. Well, we can still have fun, but let's talk about your real work. Let's talk about those Greek letters that you've got.

CO:

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. Programming languages have typically kind of 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.

CO:

But during the actual process of programming, this sort of act, this dialogue that you have with your programming environment, you're not producing complete program after complete program. You are in these incomplete states where there might be missing chunks of a program or there might be errors that you're puzzling about. Where there might be multiple people working on different parts of the program and so they're inconsistent temporarily.

CO:

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 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 and it's very nice orthogonal way where you can then study that feature in isolation.

CO:

And so, that's what we want to do with the foundations of Hazel, which we called 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 stand for, or serve as membranes around erroneous parts of the program. So, type inconsistencies, binding errors where you have an unbound variable for example, other things like that.

CO:

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. Yeah, 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. So allow you to see the values of the variables that you've bound so far while you're figuring out how to finish the program.

CO:

And so, yeah, so Hazel is 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. Now, the last few months have really been focused on scaling that up. And so Hazel is... it's still a very simple programming language and programming environment, but it's sprouting more and more features like those you'd find in full scale functional languages right now.

CO:

So we're kind of targeting Elm because it has a, it's a pure language, it doesn't have exceptions. 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's 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 codesign kinds of questions. Like, are there features you don't need because you have editors 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.

SK:

Yeah, fascinating. So much I want to reply to.

CO:

Yeah. That was maybe too many things all at once.

SK:

No, no, it's great. I love it when I interviewed someone and I know they have a spiel and then I just, you know, yeah...

CO:

I've been writing a lot of research statements and those kinds of things lately, so I've been practiced.

SK:

Well, and I can even tell when you gave the presentation at LIVE 2018, 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. I know how to explain what I do.

CO:

Yeah. I mean, I've presented, yeah, the fall 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 the freedom to explore those ideas.

SK:

So, let's, I'm going to try and remember the things I want to touch on. The first thing that struck me was that the lambda calculus is the Schrodinger's equations of programming.

CO:

Of computer science.

SK:

Of computer science. I see, yeah, well there's a difference. 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 equation, maybe he had a different-

CO:

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.

SK:

I guess, is Schrodinger's equations important or could you say, I think maybe the lisp one was Maxwell's Equations.

CO:

Maxwell's Equations.

SK:

So it doesn't really matter which equations, you're just saying it's like the foundational set of equations for our field?

CO:

Yeah. Yeah, I think so. I don't think there's really a tension between saying it's like, Lisp, its heart is the untyped lambda calculus. It's a matter of notation almost.

SK:

Oh okay. So they really are equivalent in that way. That's interesting.

CO:

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 classical lisp systems.

SK:

Were there other foundations for programming that are like in contention with lambda calculus? I know there's a Turing Machine but people don't use it for, I imagine for good reasons. Are there other calculi that are competitive or everyone pretty much agrees that the lambda calculus is the way to go?

CO:

I think everyone pretty much agrees that the Turing machine's 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 lambda calculus is the way to go, but the world's a big place.

SK:

Oh, I see.

CO:

I don't want to characterize other people's opinions on this.

SK:

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 calculous people and others aren't...?

CO:

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. So there are... you know, 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 lambda 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 typed of lambda calculus, you get a lot of mileage out of that way of thinking.

SK:

And yeah, yeah. I have a friend actually who speaks in a very similar way. I forget... There was a book he told me to read, I think it might have been written by Bob Harper.

CO:

Was it Practical Foundations for Programming Languages?

SK:

It has one of those titles that's impossible to remember because it's just like, the name of the field and the word like practical or something.

SK:

It's probably that book. So that's a great book. That's the book we teach PL class out of it at CMU. It starts like from the simply typed 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? You have just two or three pages which get to the essence of concurrency and lazy computation and imperative programming 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 insightful.

SK:

So, sorry. Is this the one TaPL? Is that how people refer to it?

CO:

TaPL a different book that has sort of a similar feel. TaPL's a little older book by Benjamin Pierce at Penn. So that's probably whereyou got exposed to that.

SK:

I see.

CO:

And yeah, PfPL is kind of the abbreviation that people use for this Bob Harper book.

SK:

Yep. Yep. So I don't know if you know Steven Deihl from Places on the Internet?

CO:

Yeah, I know him from Twitter. Yeah.

SK:

Yeah, yeah. So we met up in the real world in London and, he's been pushing both of these books on me 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.

CO:

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 invariants are you going to be able to state about the lambda calculus extended with feature, which is something you can't do without a foundation like the lambda calculus in mathematics, right? A foundation in mathematics.

CO:

So Bob likes to call like the alternative approach where you just kind of implement stuff in your favorite interpreter: seat of the pants programming language design. Right? Just like let's see what happens, right? Like, I dunno. I'm not going to prove any theorems. That's Greek and I don't speak Greek.

CO:

But then you end up with these misfeatures, right? These features that you regret and there's kind of stuck in the edifice of computing now. It's like null pointers, which the designer of that feature now regrets and it's called "the billion dollar mistake". Right? So, yeah, it gives you 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. I think it works really well. I think languages that are rooted in this process are now starting to reveal themselves as languages of the future.

SK:

That's a contentious statement-

CO:

It is, but that no one else is here to argue with me. So.

SK:

That's true, especially 'cause I agree with you, so I'm not gonna argue with you. So to get back to some of the things you mentioned I don't know if you mentioned this phrase in in your spiel just now, but I've heard you refer to it before, the gap problem.

CO:

Oh yeah.

SK:

So yeah-

CO:

The gap problem, I didn't say that phrase, but the gap problem is just this gap between 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 refers to these gaps in service. Gaps in editor services that arise because it doesn't have 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 200 different places in the program. While that whole time you're doing that, program doesn't type check, certainly can't run it, sometimes it won't parse.

CO:

And so with Hazel, we've solved the gap problem in the sense that every editor state, 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 nontrivial 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 think that doing a clean slate design is really what enables that for us.

SK:

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 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 still have no gaps. It'll still like give them monkey good editor services.

CO:

Yeah. I like to use in my talks, I have this 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.

SK:

And I think a point to just make clear is that even if like the monkey by accident put like six plus 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. So I think that's like a really cool property.

CO:

Yeah, exactly. 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.

SK:

Yup. Yup. That's another great metaphor. Yeah, you just underline the errors and just leave them there because they don't stop anything.

CO:

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.

SK:

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 that 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 that I feel like this conversation has been lacking up until now. People give some benefits to structured editors. Other people say "Oh well, we tried those before. They didn't work. They're never fluid." But I feel like 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.

CO:

Yeah. So what structured editing buys you... (Hazel's a structured editor)... 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, right?" That's actually very important to have zero. In the same way. It's very important to have these holes that like positively represent nothing being somewhere.

CO:

And what structure editing allows you to do is it makes it so you, the programmer don't have to insert the holes manually. Like in Haskell today, and several other programming systems, you can insert holes manually to make the type checker happy. Structured editing inserts holes automatically, both empty and not 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.

CO:

So you mentioned, I mean, there are structure editors who have been around for a long time. You know, we didn't invent the concept of holes or anything like that in Hazel. There have been lots of questions about the usability of these things. 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 texts that don't make any sense. You know, two plus `f`, maybe you were about to apply `f`, but that moment doesn't make any sense.

SK:

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. I'm trying to make it an inner thing or I'm like doing a refactoring where I'm really like inverting the control structure. Then there's a lot of states that just don't make any sense.

CO:

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 mbeddr, which is built using this tool called MPS that JetBrains makes, which is a structure editor-generator sort of and mbeddr is this 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 they're parentheses aren't balanced. It's just like okay, that's a kind of node: unbalanced parentheses node.

SK:

Wow, that's interesting.

CO:

Yeah. So we've taken a lot of inspiration from that design in Hazel. So Hazel is also kind of designed not to be this ... You know, there are structure editors that are like these blocks languages that kids use to learn programming. Like Scratch. 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.

CO:

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 take this sub tree of your program, temporarily render it just as text that you can edit as text. 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 the sub tree 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. That's an ongoing kind of thing that's not in Hazel yet, but we're thinking about how to do that right.

SK:

It's like you're technically you've still solved the gap problem, but in that sub node, you don't actually get editor services.

CO:

Right. Yeah. Or you get maybe some syntax highlighting based on Regex-based cloud editors do, but you don't get the full suite of editors services. Yeah.

SK:

Yeah. Well to me that feels like a stop-gap solution. Like one day, hopefully, we'll have solved the fluid structured editor problem and then you'll get rid of that escape hatch.

CO:

Yeah, it's definitely a stop gap and I think, yeah, that ... Another project that we're working on is 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 the 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 on Idris on these kinds 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.

SK:

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?

CO:

Yeah, yeah.

SK:

So I guess ... Sorry. Yeah?

CO:

Go ahead.

SK:

Did I lose you for a minute there?

CO:

No. I'm here.

SK:

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 like 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 then 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?

CO:

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 and you run it is you end up with a result with holes in it, corresponding to holes in the original program. And 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, well 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 where it needed to know what was going to be in the hole to continue. And so we developed a semantics for 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.

SK:

Yep, yep. That's exactly what I'm looking for.

CO:

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 beginning. So if you think about like if you've ever used Jupyter, IPython, these like computational notebook things where you have these cells with code in them, what you can do is you can ... It's kind of like a REPL except you can go back and re-execute cells. 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 notebook.

SK:

It's awful.

CO:

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 your analyses to be reproducible. And so this guarantee of ... We call it a communitivity. So what's commuting is editing is commuting with evaluation. Hole filling in particular is commuting with evaluation. So yeah, having that guarantee I think is a really important guarantee for reproducibility in sharing code with other people, performance and so on. What it doesn't do is allow you to change the code in ways that don't amount to hole-filling.

SK:

Oh, interesting. Yeah, that's what I was going to ask.

CO:

Yeah. So I mean that's trickier because if you've actually just changed the behavior of your program, then you almost can't get away from rerunning it or some, you know, because the behavior of the program is different. All the stuff that happened before that you want to avoid re-running would've happened differently because the code is completely different. So it's trickier to get that kind of guarantee. There are hot code reloading mechanisms that try to protect you from really egregious changes in the way your stack and heap is laid out, but it doesn't have that kind of strong guarantee anymore.

SK:

Well, I feel like the same way that you justified and contextualize what you've done with typed holes, 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 P and it's complete, they're are no holes, like P prime and P prime-prime are like fascinating because that's what the dialogue is about. I'm constantly changing. And so I feel like there should be some semantics. There should be some semantic foundation of evaluation of P and I change it to P prime and I still have your evaluation of P. There should be some way to save the...

CO:

Take the diffs and apply them to the results somehow.

SK:

Yeah, there should be some way or I don't know. Did you think the same...? You get what I'm getting ... The parallel, I'm trying to go to go for...?

CO:

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 re-running 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 and dynamic.

CO:

The complimentary question, though, 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? And I don't know how much work has been done on that. Maybe some. I'm not 100% sure. 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 functions now different. And so you can try and do some checkpoint kinds of things where you say well, until you get to the code that changed, everything was fine until you get to it in the control flow. Maybe you can like reuse kind of a prefix of the trace-

SK:

Control flow. What is that?

CO:

There's control flow. Control flows are a thing. When you take a branch in a case analysis-

SK:

That's just data flow.

CO:

Yeah. That's fair. Yeah, so I don't know. Yeah, I think that's an interesting set of questions. It's worth investigating further.

SK:

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 extension?

CO:

That's the only way to do it.

SK:

Hahaha, okay.

CO:

I mean, you could do it by the seat of your pants, but we're many decades into computing now. I think it's time for us to return to some principles.

SK:

Okay. All right, so there... I have a few more questions. So one of the questions 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? Can I just wrap the whole thing in a function and call that a parameter? Is that ... Yeah, sorry. ...What's the response to that?

CO:

Yeah, so a parameter is mediated by a variable and when you fill in a hole, it's not exactly the same thing is substituting for that variable because substitution is ... Maybe I'm getting too wonky here... Substitutions capture what you can see. When you fill a hole, you want to have access to the variables in scope with that hole. But a parameter to a function doesn't have access to the bindings inside that function, right? That kind of an egregious violation of the binding discipline of most languages. So they're not quite parameters.

CO:

There's this notion in type theory, particularly this kind of type theory called contextual modal type theory called a meta variable and a meta variable's 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 you replace the meta variable with an expression that has free variables in it that get rebound in the scope of the meta variable. 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 PoPL goes more into that.

SK:

And so, I'm going to try and repeat it and maybe I'll get it right or wrong. A meta variable is like the context. And when I say context, I mean all the variables that are in scope and their current state. So that what a meta variable is.

CO:

Basically, yeah.

SK:

It's just context?

CO:

Yeah, so the way you refer to a meta variable is with what's called a meta variable closure, which is for all the variables that that meta variable... That the thing that the meta variable stands for might use, there has to be some value for that.

SK:

Yup. Yup. A closure, yeah.

CO:

[crosstalk 00:58:11] for it, yeah.

SK:

That makes sense. Like the `this` keyword in Javascript kind of closure-y thing.

CO:

Sure... `this` keyword in Javascript...? I think of it as just like 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.

SK:

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 to to close over.

CO:

I see. Okay.

SK:

And so sometimes in Javascript you'll pass it. Like you'll pass it an object that'll act as its environment.

CO:

Oh, I see what you mean. Yeah, it's giving you the implicit, like when you refer to something not in scope immediately in that function, it goes through this, I guess? It's been awhile since I've written Javascript.

SK:

Well, yeah. Yeah, you're right. I'm not exactly sure either what I'm getting at... All I know is that you can change the meaning of `this` by like specifically saying ...

CO:

Like doing `this.apply` thing. Yeah.

SK:

Yeah, what is it called in Java...? Well, I know that with the fat arrow, it does that automatically... No, but I think [crosstalk 00:25:22]-

CO:

Yeah, there might be some relationship there. [crosstalk 00:59:24] reminding this. Yeah. Yeah, I mean, the real kind of elegant relationship is with this contextual model type theory, which is 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 this particular logic talks about necessity. Like it's sort of the analytic philosophers way of talking about what's necessary for this thing that I'm talking about to be valid.

CO:

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.

SK:

Yes. I want to get more into that later: the generality of theory. I'm excited to do that. But I just want to finish up with Hazel. Let's see. Well, one of the things that you alluded to that I want to get back to is the Palette work that you started your career worth. 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 what part of what you ran into is that one thing that was hard about building those sorts of augmentations is the gap problem. Is that where you first went into it? And then that's kind of what inspired this project or am I just projecting onto your experience?

CO:

Yeah, sort of. So like when in Eclipse, you know the way the Palettes were sort of presented to you was based on the expected type at the cursor. But of course what that requires is that has to exist, that Eclipse needs to be able to tell that to you. And if they 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 as internally inserting holes to be able to offer you that kind of expected type when you've just typed like `f` open parens.

CO:

That doesn't parse according to the grammar of Java, but Eclipse doesn't completely barf, right? 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. 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.

CO:

In Hazel, 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. Yeah, so then the Palettes, what was limiting in the clips setting with Palettes, there was a few things that we're trying to improve with Palettes and Hazel. So one is Palettes and Eclipse are ephemeral. So once you're done interacting with the Palette, once you've written your regex and your tests or when you've written and 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 like 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.

CO:

And so in Hazel, because that you're editing an AST directly, 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 like things that are in the program that you are 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 possible 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 and you're sort of trying to turn Eclipse into structure editor at that point.

SK:

So for that regex example, if you are in Hazel and you write a regex, write some test examples and you're going along and then you ... Where are you storing those test examples? Is it like some metadata attached to the language somehow or it's like there's a hot... How does that work?

CO:

So 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 it, in the AST itself, at the place where the Palette is generating code, it's just keeping that model like ... But like a serialized version of that model. Although there's not a lot of actual serialization necessary because it's just a Hazel value.

CO:

Yeah. So that's the design that we're working on right now is just ... In the AST, if you just looked at the ASDTkind 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 function is to update the model. And then also there's a function called `expand` that takes the model and generates Hazel code, which is what the meaning of the semantics of that Palette is, is the code that it generates.

SK:

Oh, okay. So if you have a Palette in the tree, there doesn't exist the expanded code by itself?

CO:

Right. 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, entering that into a view as needed.

SK:

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 is the canonical representation and then the expanded view is just like something that it produces.

CO:

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 is 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 'cause it's a macro system really. And how to reason about the rest of the program in the presence of these Palettes, right? Because 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 typed macro systems that apply also to this Palettes mechanism. And so, yeah, I think of them as kind of graphical literals. And then that brings up another thing that we're trying to add, which is you might want expressions inside the GUI.

SK:

Yeah. You took the question right out of my mouth.

CO:

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, just literal numbers. Right? So in Hazel, we're having it be totally compositional. So if 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.

SK:

When you say in and out, you mean your cursor can go in and out? Or you mean that you can't ... Can it look like a nested structure where I can see an outer structure and then it's like an inner structure? It's nested boxes? All on the same screen and my cursor can just move fluidly?

CO:

Yes. Nested boxes, basically. So you can imagine there's a palette for generating numbers by manipulating a slider. Right? Really simple example. Then you could have a matrix of sliders, right? You'd want to be able to do that.

SK:

An what if I want a matrix of sliders and each slider is multiplied by 10. Can I do-

CO:

Yeah, yeah.

SK:

Mathematical expressions?

CO:

Mm-hmm (affirmative). You can put that slider anywhere a number's expected. So inside an arithmetic expression, it could be like slider times 10.

SK:

Perfect. Perfect. Beautiful. Oh wow.

CO:

There's some questions about how to lay out stuff like that once it gets really deep and ... Yeah, layout is a tough question actually. But conceptually, it's working.

SK:

Yeah. Well, so then all of the sudden ... It begs the question of what is the difference between an expression and a GUI. And I feel like 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 a full expressed control over the layout, then all the sudden, you've done it. You've blurred the line between GUIs and programming. Because-

CO:

Yeah.

SK:

Yeah, the-

CO:

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.

SK:

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 the sudden the expression is GUI things and you care about the way they are laid out, then all of the sudden you want to be able to manipulate these things as data. That's fascinating.

CO:

Yeah. It's definitely very ... I mean macros are the foundation for this mechanism. It just adds a bunch of stuff. And 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 ... 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 axis labels. It has some data and it has some color parameters for different lines and so on. And those are all things where you could imagine like maybe it's nicer to directly manipulate that plot, edit the text and the colors of stuff in line.

CO:

But the purposes of the plot is to plot some specific piece of data. Right? You can create an abstract plot with some abstract data, and then run that program and get the actual plot. But it would 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.

CO:

And so while 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 and scope. While 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 can say, "Okay, I know you want to plot this particular piece of data. I'll just show you it right here in the middle of your programming," instead of waiting for you to run it and seeing 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, it's something that we're working out how to do right now as well. It's really based on the work we've done on my programming already.

SK:

Yeah. Yeah. So I really love that part of your work, that you have not only the static abstract code, but live data. How will that... But I missed the significance of how that would be interesting in the context of a palette?

CO:

The purpose of 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's eventually going to do when it's run.

SK:

Mm-hmm (affirmative). Yep.

CO:

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 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 that's why it's really useful to have that live information and to run the program before it's done. Like before the palette's even kind of, before you're done interacting with the palette, you could still run the program. And get the information that the palette needs to give you even better assistance.

SK:

I see. Cool.

CO:

So I think there's lots of examples of 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 inline inside your program.

SK:

Just for the feedback?

CO:

Just for the feedback. The code it generates might even just be like unit sometimes.

SK:

Mm-hmm (affirmative). Cool.

CO:

Or it takes the argument and gives it back to you... it behaves as the identity function, but its display gives you information.

SK:

I feel like that that's kind of equivalent to console.log. If the behavior you want is "Just show me the value of this thing," I imagine that there should be an editor magic that does that without having to-

CO:

Yeah. 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 particular way of displaying this type of thing.

SK:

That makes sense.

CO:

Where you want some control over that.

SK:

So one quote that I ... I think I pulled out of one of your papers, was you talked about recasting tricky language mechanisms, as editor mechanisms.

CO:

Oh, yeah. 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 just dump entire set of bindings from this library, which might change, into your scope. And the code evolution's really difficult because things start shadowing each other and so on.

CO:

And the only purpose of import star is because you're too lazy to explicitly qualify everything as a programmer. And that's totally legitimate, right? That's the kind of laziness that, like eating your porridge, right? It would 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... 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 telling what's in scope and so on. So that's one example.

CO:

Another is there's this whole set of language mechanisms around implicit parameter passing. So type classes are actually really just implicitly your 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 also developing an implicits, modular implicits, which is a way of passing first class modules around implicitly for many of the same purposes of Haskell and Scala.

CO:

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 convenience. I don't want to pass these things explicitly. What if that implicitness was just part of the editor, where 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 this implicits in it. It's just still the very, very easy to reason about semantic model of, say, ML. Right?

SK:

Yeah. That's a fascinating idea.

CO:

Yeah. I think sort of, yeah. I don't know if it will work, but it's something to think about it at least. And having this codesign 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 editors side."

SK:

I wonder what you lose if typeclasses are now implicit. Like it feels like ... I could be wrong but to me it feels like typeclasses in Haskell are this almost like a tool to reason about and they have certain laws. They're like ... They're more than just the sum of their parts somehow. And I worry if the language doesn't actually talk about these things, then maybe the editor will be forced to do these Eclipse-like heuristics to map backwards to typeclasses, when you could have just put them in the semantics.

CO:

Yeah. So type classes are really just kind of an impoverished module system in a lot of ways, right? 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 typeclasses. There's a mechanism in OCaml, a modular that's being developed in OCaml called modular implicits, and it's based on this paper called Modular Typeclasses, which separates those two aspects of type classes. So the implicit passing of things is one part of the type class mechanism and that's sort of bundling functions together to talk about a type. That's sort of an abstract type. It's another aspect of type classes and-

SK:

Interesting.

CO:

And those two things don't need to go together.

SK:

Okay. And the thing that I was worried about losing is the abstract bundle.

CO:

Yeah. You were worried about losing the module system aspects of it, and I think those things come from having a proper module system. The Haskel world has sort of slowly started to realize they need a module system. There's this project called Backpack, which tries to back patch a module system into the OCaml or into the Haskel build system basically. And yeah, it seems like an interesting approach. It seems like it will work out, but it's a lot nicer to have it be actually a part of the language than at the level on only package management.

SK:

Yeah, Got it.

CO:

So with Hazel, we want a proper module ML style module system at some point. Development of Hazel is very rate limited by just how much time a 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.

SK:

I see. And I guess ... And I don't know if you're the right person to ask this question to. But as far as the typeclasses laws go, are there any programming language semantics that have laws embedded in the language itself? Or without, like only be a language like Coq or something.

CO:

Yeah, I mean when you start talking about the equational behavior of functions, you need a type of system that has support for reasoning about equational behavior. And then you're doing a dependently typed programming. There are refinement type systems that have sort of a ... So, refinement type systems are kind of between certain sense, sort of simple type systems and dependent type systems where you can say, "This is an int such that X is an int, such that X greater than zero." And you define this predicate on values of that type int, and there are ways to ... There's some really cool work in Liquid Haskel on kind of encoding the equational proofs into ... refinement type systems, which are actually simpler in some ways than full dependent types. It's some work by Niki Vazou and Ranjit Jhala and some other folks. But yeah, it's difficult to actually ... Yeah, Liquid Haskel is probably the thing that would maybe answer your question, if you want to stop short of full dependent types but still reason about type class laws.

SK:

Mm-hmm (affirmative). Got it. Yeah, a lot of people pushed me to Liquid Haskel and dependent types and refinement types. So I probably should actually learn what these words mean at some point.

CO:

Yeah, I mean so verification of these 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 that's another thing that we haven't done much with in Hazel yet, but editor integration of these kinds of things where it helps you discover the invariance and then prove them correct, prove your code correct. That's another kind of frontier of PL research that has a lot of foundational research already done. It needs to kind of be put into practice inside an editor.

SK:

So speaking of foundational PL research, I think now's maybe a good time to ask you to defend it. Because I think there are a lot of few ... I don't know if, 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, this guy's just like an academic, who's just proving abstract properties of things nobody cares about."

SK:

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. 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?

CO:

Yeah, there's a lot there. There's a lot of different views on Greek letters in math and its value. I mean if you step away from CS, if you told a physicist that math is superfluous, you'd get laughed out of the room, right? Because you can't do physics without math. And as you get more towards sort of the human sciences, people become more and more hesitant to involve math. And I'm not sure that really makes sense, right? Obviously, there are other things that you have to involve when you start talking about designing things for the 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're just flailing in the dark, right? So, I think-

SK:

Just I was going to say that I feel like part of the quick counter-argument to that is there a lot of people who make a lot of progress, making billion dollar businesses or whatever, doing programming and not doing the math stuff.

CO:

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 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. You copy it in and you see if it works. And you feel the benefits of it. And yeah, that's fine. You can build bridges without understanding calculus. That doesn't mean you can build the Golden Gate Bridge without understanding calculus. 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.

CO:

Then the other question is yeah ... So, okay, 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 PL papers, I didn't even know what the letter was. No one had ever taught me the Greek alphabet.

SK:

So, you're not in a frat?

CO:

Right, that's the only background I had. I wasn't in a frat, but I went to the 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. Yeah, I think that really a trait, 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. So it's just a circular kind of situation where no one ever learns how to read the papers that we're writing. So they are very difficult to read, if no one's ever taught you how to read them.

CO:

But there's also this failure of expectations, right? If you see 10 pages or five pages of a paper, then 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 a 10 page mathematically-dense paper in the same amount of time it takes you to read 10 pages of a novel.

SK:

That's well said.

CO:

You shouldn't come in with that expectation, right? You should think of mathematical notation as 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 a hundred pages decompressed or more, right? I don't know what the compression ratio is for type theory, but it's pretty high.

CO:

But what's great is, once you've started doing that, the compression long enough, it happens in the sort of sub-conscious. And then you can read these things very quickly, because your whole brain is engaged and 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.

CO:

If you look back at the history of mathematical notation, which is very interesting, Euclid's elements, it's like three thousands 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, long-hand. 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 this full sentences that are like "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, it wasn't obvious that there was this other way to do it that would be initially a little imposing, but eventually much nicer.

CO:

It wasn't really until even the 1600s when the printing press and all these things started democratizing learning about these topics that people said, "Do we really need to 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 so slowly more and more abbreviations started entering. It wasn't matrix notation. It was like late 1800s and by Lebniz had some calculus notation that's persisted, which I don't actually think is very good.

CO:

And it's really earlier than that. 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 civil engineers to understand calculus without taking three semesters or more of it. I think we need that same expectation for... Learn how to program without the math, of course, right? 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.

CO:

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 ... I 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.

SK:

Yeah. Well, I think that's quite a good pitch for studying math. So would you have some concrete places to start learning, like we already mentioned TaPL and Bob Harper's book. What are the other-

CO:

Those are great starting points. You don't even need to read the whole book, right? I think the first quarter of the book is enough to pick up many PL papers and start to understand them. I do wish we had more ... Like I was saying at the beginning. I wish we had more surveys and introductory material in places where you take all the contributions that exist in papers and bring them together as sort of WiKi idea. And so I hope one day to be involved in building such a thing. But for now textbooks are great.

CO:

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 and papers aren't written 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? My papers are written for people that have read the first quarter of those textbooks. I'm not going to try to rewrite those textbooks in the intro section of every paper that I write. That would be a colossal waste of time and space.

SK:

Well, that's actually an interesting ... I have an interesting lens on that thought, because a few weeks ago I spent a long time on an introductory paper to a very dense mathematical topic. I tried to write it for a general audience, and it did not go well. I think part of the issue was I was writing about complicated subject, but with the tone of, "You'll be able to get this if you just read my writing." And now I kind of wish ... I'm considering putting up at the top of the article, "If you don't already understand these concepts, don't read this article."

CO:

Yeah, that would great. I wish we had more of that. Here are the prereqs for this paper. Please make sure you at least look briefly at these things first.

SK:

Yeah, because it's crazy. When I go to install a piece of software and they're like they don't list the prereqs, what I need installed ... I hit install and it just gives me an error like this thing isn't installed. So how could you know? This is a prereq.

CO:

Yeah, yeah. Somehow this is a very difficult problem in computing: dependencies.

SK:

Yeah. So I guess what I was getting to is that Greek letters and like certain things like that kind of do that by proxy. It's like, if this scares you, you'll just stay and learn on your own. You don't need the warning sign.

CO:

Yeah, maybe. But there's ... But Greek letters are used in all sort of different domains, right? It's basic type theory that uses Greek letters, but there's other ... There's papers written where you just to have read other papers in that a field and there is no textbook or there's no survey paper. I think that's a shame, but that's still true. And those are the papers where I think you really need this kind of 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.

SK:

Yeah. So thank you for your defense of theory. Oh, actually, there was one other thing that I wanted to tee up for you. I remember when we were in Boston together. I asked ... I forget what it was that I asked you, but I mentioned something about why are you working on theory. It was a similar question of defend your profession, defend theory. And your response was theory has its generality. It might not work with the tools of today and the fads of today. Theory has this ... It will be around for forever and it will be applicable in many different domains.

CO:

Yeah, exactly. So 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.

CO:

And the future's a very big place compared to the past of programming so far. Even the past of mathematics so far. Hopefully, right? Hopefully, humanity survives. It seems inevitable that at some point someone else will want to develop a structure editor. It would be very ... I would need a lot more confidence 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 just need to do it once, and that's it. Right? So the generality aspect is: the future is much longer than the past so we should be writing for the future.

SK:

Well, then it's almost like why waste your time building Hazel, because it's just one shot in the dark? And there's an army of people in the future that might build things. Why don't you just ...?

CO:

There's lots of theoretical questions that will come up as Hazel develops further. And we'll write papers about those things that would be relevant to people in the future that come up on the same problems. I don't want to understate ... I do want ... I think we're in a very important part of history here at the beginning of computing, where the choices 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.

SK:

It's almost like a backup plan, worse case scenario. Yeah, because I guess if you just wrote your insights into code, nobody's going to go back and parse them out of the code and put them into their next thing.

CO:

Yeah, 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 thousand lines of poorly structured Haskell instead. Right? That will take you a lot more time than it takes you to read 10 chapters of a textbook and then 12 pages or two papers worth of Hazel stuff. So Hazel's written on OCaml so right now. Hazel's very austere, but it's still about 25 thousand lines of code, the implementation.

CO:

That's going to take you a lot longer to read than our 25 pages of paper, and it's going to be a lot harder for you to get the essential ideas out of that codebase than it's going to be to get them out of my papers, hopefully.

SK:

Hopefully.

CO:

Yeah. I don't know.

SK:

I think that's a pretty good pitch, math is compression, what you said before.

CO:

Mm-hmm (affirmative).

SK:

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 multiple people editing the same codebase at the same time.

CO:

Yeah. Yeah, that's something I'm really excited about. 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 ...

SK:

Oh, so the cursor is part of the edit semantics? It's formally represented. Like when your cursor's here-

CO:

Yeah.

SK:

Oh, interesting.

CO:

Yeah.

SK:

That isn't obvious to me, because I would almost think of having edit semantics that's like a bird's eye view semantics.

CO:

Yeah. There's other ways to represent where the cursor is than we choose. I think you want a cursor or multiple cursors. You don't want the edit actions to just be... they need a locus of action. Your edits are happening somewhere.

SK:

Well I guess now, that obviously makes sense based on the way that we edit code now and text editing. But now I'm wondering 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 to locus of action. So a cursor seems to make sense.

CO:

Yeah. It's hard to imagine doing transformations on the whole program from the top without referring to a place in the program.

SK:

Yeah.

CO:

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 the selected unique ID is effectively the way you're representing the cursor. So it's isomorphic in that way.

SK:

Okay.

CO:

But yeah, so with collaborative editing, right, you want to have multiple ... one way to put it is you want that multiple cursors. Another way to put it as you want to have multiple replicas of the editor state, where maybe you need to replica this one cursor, like each person has their own replica and their own cursor in it, but then you want some way for the ... in each replica, you're editing it by creating this history of edit actions. That's changing the code, and you can represent that change by a structural diff, but really the things that caused that change are the edit actions that you performed on that replica.

CO:

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 Doc 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 combine things right now is these structural diffs, which often obscure what you actually did, because it needs to be edit without any notion of history.

CO:

So what if we represented change, 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 that you figure out using Greek, that says that there's a convergence if you merge these replicas, and you're leaving the sequences of edit actions, you get an equivalent output for some notion of equivalence.

CO:

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 happened to those two replicas by choosing three arbitrarily or choosing four arbitrarily.

SK:

Yeah.

CO:

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 edit actions available to resolve conflicts, and those go through the same process.

CO:

So it's kind of like when git inserts these 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.

SK:

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.

CO:

Yeah, exactly.

SK:

Very cool. So you're taking all of the auxiliary tools and programming, and you're putting them into the semantics of the language itself.

CO:

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.

CO:

And yeah, what this is all related to is this notion from distributed data structures called a CRDT, which stands for Conflict-free, or sometimes Convergent Replicated Data Structure. And so there is theory, there's some nice papers starting about in 2011 on CRDTs for much simpler data structures like sets, like insert-only set. It doesn't matter what order the insertions come in, you can replay them in any arbitrary order and you'll get the same set.

CO:

So what if instead of the data structure being something very simple like a set, what if it was a typed expression in the lambda calculus or in some extension of the lambda calculus? So that's kind of the research question there: can you make a CRDT for this very semantically rich data structure?

SK:

Yeah. That does sound like a hard question.

SK:

And to your point of it's worrying to reinvent everything about programming ...

CO:

Yes.

SK:

I see that that's a worrying thing for you to do by yourself. But I do like the idea of reinventing everything that has to do with programming that's now on the side, like it's been ad hoc, seat of the pants, "Well this language doesn't do this thing, so let's put it in the editor, and let's ..."

SK:

I really like the idea of taking all those things and putting them into semantics so we have mathematical confidence about these things. And to to the point that you said earlier, 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, a lot of them are orthogonal.

SK:

Once we've, as a community, agree upon the fact that we're going in the structured editor direction and we care about programming experience and we care about embedding everything about programming into mathematical semantics, then all of a sudden researchers can be freed up to work on ... someone else can work on the CRDT problem, and you don't have to worry ... when they're done, you can import their Greek letters into your codebase.

CO:

Yeah, yeah. I think, yeah, this is an underappreciated benefit of having a thing like the lambda calculus, is in many ways it's the most widely used programming language in computer science research. Because so many researchers build on the lambda calculus, much more than there are researchers that build on any particular programming language. And all that work is going towards this common vision that's emerging, where 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 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 you make this all make sense together.

SK:

So there are a few things, but one in particular idea I've had for improving programming, that not until this conversation did I think like, "Oh, maybe I should prototype this on top of the lambda calculus, instead of in a broader, seat of the pants experiment." You know?

CO:

Yeah.

SK:

Maybe you'll just point me to literature where there's already exists: where the terms in a programming language are referred to by the hash of their definition.

CO:

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. Yeah.

SK:

Does the lambda calculous have definitions, or it doesn't have ...?-

CO:

It doesn't have definitions in the sense of type definitions or module definitions or anything like that. There's no sense of labels.

SK:

Yeah. So that's what I'm wondering. This feels like sort of a labely thing.

CO:

But you can, 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.

SK:

I guess maybe the broader question is, are there some times where 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."

CO:

I'm not opposed. I write code in the context of experimentation sometimes before I do lambda calculusy stuff.

SK:

Wow. So risque.

CO:

So I'm not opposed to that. Yeah. I don't do it that often, actually. I do mostly start on paper with the lambda calculus, to be honest.

CO:

Definitely user interfaces. I work on the underlying mechanisms, the semantics for the live programming and all this stuff. There's a bunch of UI stuff that 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. There's not a lot of ways to do mathematics for UI stuff.

SK:

Yeah, UI stuff. Yeah.

CO:

Yeah.

CO:

So if it is a UI experiment that you're doing, by all means, do a UI experiment with code, or with other methods like mockups. We did some mockup stuff in that paper we were talking about.

CO:

As far as ...

SK:

Well I guess part of-

CO:

You're talking about content addressable coding, right?

SK:

Well yeah, and part of why I was inspired to ask this question is before this conversation I never thought of git, which seems very much orthogonal to editing, orthogonal to the semantics of a language. The semantics of language, I thought, was about how to evaluate the language. And all of a sudden, you're like, "No, actually, if we have an edit semantics, now all of a sudden, git has like formal semantics, look at that."

CO:

Yeah. Having a semantics around edit actions is so beautiful. It gives you this way to talk about change and programming and all this stuff that we've just thought about informally.

CO:

If you think about it, 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, you're going to say it's going to be seven plus whatever you're going to write.

CO:

But until very recently, we had no way to say that formally. And it's the same way with edit actions. 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 mathematics. 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.

SK:

Usually, when I see your presentations, when you talk about collaborative editing, the next place you go is also very exciting to me. You talk about this computational Wikipedia.

CO:

Yeah, yeah. Well we started with that almost ... yeah.

SK:

So that was almost like a scientific Wikipedia. Actually, you're right, computational in that ... well, 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 it'll run some code and give you the results. It's like Wikipedia, but it's also Jupyter Notebook. And I think that's like, whatever, it's kind of cool. It's like not only can you embed pictures, you can also embed code.

CO:

Right. Which I think that would be useful, but that's not exactly what I have in mind. I have something grander in mind.

SK:

Yeah. I think one of the things you said about it that stuck with me is what if we ... I don't know if that's what you meant ... if you imagine all of software as being somehow connected, it's like all the different software is just one single piece of software, and it's all being edited collaboratively at the same time, and yet, when one person is in the middle of an edit, not everyone else's computer is crashing.

CO:

Right. Yeah.

CO:

Imagine something the size of Wikipedia or the size of the Internet, which is actually formally a single mathematical expression, just a 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. So one person editing one page and stopping in the middle of what they're doing and getting some coffee, 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.

CO:

So 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 separate siloed programs and pages and things serve today?

SK:

Mm-hmm (affirmative).

CO:

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 conceptually I think it's doable.

SK:

Yeah. It's funny, you and I are quite similar in that my vision for the future of software also is quite similar in that a single expression can represent this really rich, complicated GUI, that can represent all of software, basically.

CO:

Yeah.

SK:

I don't think I personally thought of putting all of software in the same expression. I think of it as the same medium. Basically like on GitHub, how you have different projects, to me, those boundaries always felt artificial.

CO:

Yeah.

CO:

When I say this, sometimes people ask me about versioning. If someone's editing a library that you rely on, then it's going to break your code, and this could be chaos, right?

SK:

Yeah.

CO:

There's ways to solve that by pinning things to different versions and all this kind of stuff, but I want to embrace the chaos of it. I want my code to break cause someone else is editing another page on Wikipedia, and then I want them to come over and help me fix my code, and I want to go over there and 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.

SK:

Oh, that's interesting.

CO:

Yeah. I know you can do that, and in other settings those mechanisms might be necessary. But for something like Wikipedia, just embracing this the life that this artifact has, I think is something that I'm really interested in.

SK:

Huh. Yeah. I like that sentiment, even just to push us to think about what would have to be true in order for that to be viable.

CO:

Yeah.

SK:

Because I think you could look at Google Docs as doing that. It totally embraces ... and the reason Google Docs is able to do that is because it's solved the gap problem. There's no point at which a Google Doc will break. 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, there's nothing you can do in paragraph seven that's going to really screw with paragraph one too badly.

SK:

So in theory, once the gap problem is solved, potentially it may be a lot of the issues in terms of why we fork code and version code go away.

CO:

Mm-hmm (affirmative). Yeah, I think so. Some of the issues won't. You need good refactoring tools. You want to 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?

SK:

Yeah, of course.

CO:

Doing it without good refactoring tools is probably going to annoy people, but there's another set of research problems, is: how do you make good refactoring tools in that setting?

SK:

I think that that's part of what I like about your sentiment. Instead of saying like, "Oh well, any refactoring is going to be messy, so let's just pin things to versions, because that's its own problem, instead of that, let's challenge ourselves to make refactorings so good that we don't need to pin things to versions, things will somehow just evolve beautifully over time if you give people the right tools."

CO:

I don't want to say it's going to be beautiful. I think there will be chaos. That's why I use the word chaos. I think sometimes it'll be annoying, but that's okay. It'll be beautiful, the whole thing together will be beautiful, even if pieces of it are sometimes annoying.

SK:

Mm-hmm (affirmative). Cool.

SK:

So before we sign off, I wanted to hear an update of your academic life, and how ... because I think last time we talked, you were applying to jobs as a professor, assistant professor?

CO:

Yeah. Right, I'm looking for-

SK:

I just want to contextualize. The people who listen to this podcast are interested in programming, computer science in the future of programming. I think a lot of us go out about it in different ways. So I think that 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.

CO:

Sure. Yeah. So I'm looking for tenure-track faculty positions as an assistant professor, primarily. I'm looking for a place where I can do this kind of work, where I can, when a theoretical question comes up, I work out the theory, and I also get the opportunity to work on these long-term visions and these experimental platforms that maybe aren't immediately useful. And academia is one of the few places where that kind of thing is at least nominally supported.

CO:

I applied to 54 places, just all over the place.

SK:

Now way.

CO:

Yeah.

SK:

Was this like you just checked 54 boxes and hit apply, or you had to actually do 54 applications?

CO:

So to submit ... yeah, a lot of the material is the same. You write a research statement that's three or four pages about what research you've done and what you plan to do in the future and why it's important and interesting, and then you write a teaching statement, which is a 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.

CO:

And a few places have a diversity statement now, where you talk about ways you're working to broaden participation in computing and your research. And then you write a cover letter for each place. The form of the cover letter is the same for each place, but you say something specific about each place. So each application took between 10 and 30 minutes individually to write that cover letter basically, and to do the research.

CO:

So it was a lot of work in writing the research statement. It's three or four pages, but it took as much time as writing a full paper did for me, because you have to put a lot into those pages. It was a couple of months, basically, that was my main project, applying to these jobs.

CO:

And yeah, those applications were due mid-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. Different departments have different areas in CS that they're really focused on. A lot of things nowadays are very focused on AI and machine learning, and cybersecurity is a big thing. There's always funding things that you have to now start thinking about, like who's going to fund the work.

CO:

It's very much like ... a lot of people make an analogy between being an assistant professor and starting a start up. 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 you're not doing work that's been done in the 80s. If somebody works on structure editors, a lot of senior faculty are like, "Oh yeah, I remember the Cornell program synthesizer in 1982."

CO:

And I'm like, "Okay, well I read about that as well. And I think we're doing some new things."

CO:

But you have to convince them that you're not just unaware of and retreading work that's been done in the past that is already finished. So yeah, it's unclear. You're writing these things for people you don't know, you don't know who's going to read them, you don't know how they're gonna respond. So it's pretty stressful.

CO:

But the goal, 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 think too much about quarter to quarter stuff, the way you have to in most companies.

SK:

Yeah.

CO:

And that's the real benefit of doing it in academia. That, and the colleagues that you have. You have people that very smart, read papers, could point you to papers that are relevant to you, that you can talk to you in terms ... they've all read the textbooks, they can talk to them in Greek on the whiteboard.

CO:

So yeah, it's definitely ... for people that are interested in the future of coding, it's definitely worth considering 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 do this work on their own, like you, and a lot of other people in the live community, but it is an option. There is support for this kind of work.

CO:

I write papers about this kind of stuff that we're talking about to conferences like PoPL, which are very much theory conferences, and there's a ton of excitement there. People are really like happy that someone's bringing these problems to them using tools that they've developed. So it's not like I'm being antagonized for working on these user-facing problems. I feel supported by the research community.

SK:

Well that's great. That's awesome.

CO:

Cool. So let's finish up with a final question, more logistical than anything else. Where are the places on the internet that people can interact with you, and which ways are you looking for people to interact with you?

CO:

Sure. 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, N-E-U-R-O-C-Y. And I'm reasonably active on there, unless... I had a new year's resolution to be less active on Twitter, so I'm less active on Twitter now.

SK:

It's funny, to like-

CO:

[crosstalk 02:09:54].

SK:

I wonder what it's like to start a company where people's new year's resolution is to use less of your product.

CO:

Yeah, exactly. I hope Hazel's not in that camp one day, like my goal is to waste time on Hazel less.

SK:

Well, I don't know if anyone's like, "I really just got to spend less time on Wikipedia. It's just too much of my time."

CO:

I've had that thought. I remember procrastinating on studying for tests in college and on Wikipedia. So maybe it'll be like that.

CO:

If you're interested in Hazel and getting involved in the Hazel Project, we're definitely open to that. We have a Slack channel that I'm happy to invite people to. It's got about 50 people in it right now, so it's a lively place.

CO:

And yeah, we've been talking about there's a bit of an 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 a 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.

SK:

That's a very generous. That sounds like a...

CO:

Yeah, it's a nice ... 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 I'm very open to this mentorship kind of thing in the Hazel Slack, and in other ways. Yeah.

SK:

Cool.

SK:

Alright, well thanks so much for your time. This was a lot of fun.

CO:

Yeah, this was great. I really enjoy your podcast in general. Really. Thanks for ... this is a great service to our community, I think.

SK:

Oh, wow. Thank you. Thanks for listening. I am glad it appeals even to someone as seriously [inaudible 02:12:08] as you.

CO:

I want to get away from that like, "Oh, you're elite because you know Greek." Let's democratize Greek. Greece was known for its democracy. Let's democratize Greek.

SK:

Well said, well said.

SK:

Alrighty.

CO:

Alright, yeah. Thanks, Steve.

SK:

Thank you.

SK:

If you enjoy these conversations, I'd bet you'd fit right in to our online community. You can join our Slack group at futureofcoding.org/slack, where we chat about these topics, share links, feedback, and organize in-person meetups in various cities, New York, London, San Francisco, Boston, and also Kitchener-Waterloo in Canada.

SK:

If you'd like to support these efforts, there are a few ways that 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 @SteveKrouse so I can join the conversation.

SK:

I also accept support directly on Patreon at patreon.com/stevekrouse. 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.