Episode 1: Programming Languages

Adrian Sampson, Alexa VanHattum, and Rachit Nigam of Cornell’s Capra group join me to discuss their differing perspectives on what the research field of Programming Languages (PL) is really about, what successful PL research looks like, and what got them interested in working in the area in the first place. We also talk about some of their recent research work on programming languages for hardware accelerator design.

Consider subscribing via email to receive every episode and occasional bonus material in your inbox.

Soham Sankaran’s Y Combinator-backed startup, Pashi, is recruiting a software engineer to do research-adjacent work in programming languages and compilers. If you’re interested, email soham [at] pashi.com for more information.

Go to transcript
Note: If you’re in a podcast player, this will take you to the Honesty Is Best website to view the full transcript. Some players like Podcast Addict will load the whole transcript with time links below the Show Notes, so you can just scroll down to read the transcript without needing to click the link. Others like Google Podcasts will not show the whole transcript.

Show notes

Participants:

Soham Sankaran (@sohamsankaran) is the founder of Pashi, and is on leave from the PhD program in Computer Science at Cornell University.

Adrian Sampson (@samps) is an Assistant Professor in the Department of Computer Science at Cornell University. He works on programming languages and computer architecture.

Alexa VanHattum (@avanhatt) is a PhD student in CS at Cornell who is advised by Adrian Sampson. She works on systems programming languages, applied formal methods, and usability for programming tools

Rachit Nigam (@notypes) is a PhD student in CS at Cornell who is also advised by Adrian Sampson. He is interested in tools and languages for hardware design.

Adrian, Alexa, and Rachit are all part of the Capra Group (Computer Architecture and Programming Abstractions) at Cornell, which Adrian directs.

Material referenced in this podcast:

Logic for Hackers/Logic for Systems at Brown University: 2014 edition, 2020 edition.

The Structure and Interpretation of Programming Languages, commonly known as SICP, which is an influential introductory textbook based on MIT’s original Introduction to Computer Science course, taught in the functional programming language Scheme. It formed the basis for introductory CS courses across the world, and though most such courses have been phased out, Soham’s intro to CS course at Yale, CPSC 201, continues its legacy to this day.

Higher-order functions: functions that take functions as input and/or return functions as results.

Adrian’s 2010 OOPSLA paper Composable specifications for structured shared-memory communication. Full text of the paper available here.

Rachit’s Dahlia paper from PLDI 2020: Predictable Accelerator Design with Time-Sensitive Affine types.

Very High Speed Integrated Circuit Hardware Description Language, better known as VHDL: a hardware description language to specify digital circuits.

Hans Boehm’s 2005 PLDI paper Threads cannot be implemented as a Library.

Flatt et. al.’s Programming Languages as Operating Systems from ICFP 1999. This paper was alternatively titled Revenge of the Son of the Lisp Machine.

Caroline Trippel’s 2018 MICRO-51 paper CheckMate: Automated Synthesis of Hardware Exploits and Security Litmus Tests.

Daniel Jackson’s Alloy, an “open source language and analyzer for software modeling”.

John R. Ellis’ 1985 Yale PhD thesis – Bulldog: A Compiler for VLIW Architectures.

Transcript

[00:00:00]
Adrian: There’s something about programming languages – it’s like a lens of looking at problems that is uncompromisingly precise. We’re all just huge nitpickers – we really want to actually understand how things work instead of getting just a rough notion of how things might go.

[phone rings, number dials]

[00:00:21]
Soham: Welcome to episode one of Segfault, from Honesty is Best. Segfault is a podcast about Computer Science research. I’m your host, Soham Sankaran.

I’m the CEO of Pashi, a start-up building software for manufacturing, and I’m on leave from the PhD program in Computer Science at Cornell University, located in perpetually sunny Ithaca, New York. Computer Science is composed of many different areas of research, such as Operating Systems, Programming Languages, Algorithms and Cryptography. Each of these areas has its own problems of interest, publications of record, idioms of communication, and styles of thought, not to mention, one level deeper, a multitude of sub-areas, just as varied as the areas they are contained within.

This can get extremely confusing very quickly, and I certainly didn’t know how to navigate this terrain at all until I was in graduate school. Segfault, in aggregate, is intended to be a map of the field, with each episode featuring discussions about the core motivations, ideas and methods of one particular area, with a mix of academics ranging from first year graduate students to long tenured professors. I hope that listeners who have dipped their toes in computer science or programming, but haven’t necessarily been exposed to research, get a sense of not only the foundations of each area - what work is being done in it now, and what sorts of opportunities for new research exist for people just entering, but also what it is about each specific area that compelled my guests to work in it in the first place, and what the experience of doing research in that area every day actually feels like.

This is the map of CS that I didn’t even know I desperately wanted in high school and undergrad, and I hope folks who are just starting their journey in computer science will find within it ideas that will excite them so much, and so viscerally, that they can’t help but work on them.

Without further ado, here’s episode one - Programming Languages.

[ringing tone]

[00:02:05]
Soham: Welcome! I am with Alexa VanHattum, Rachit Nigam (via the magic of internet telephony), and professor Adrian Sampson, a subset of the CAPRA group at Cornell. If you want to just briefly introduce yourselves?

[00:02:21]
Adrian Sampson: I’m professor Adrian Sampson, no one has called me that in a year!

[laughs]

Adrian: Thank you! I’m a professor of computer science. I do a combination of programming languages in computer architecture.

[00:02:34]
Alexa: I am Alexa. I’m a second year PhD student here at Cornell. I study computer science. My stated interest is programming languages, but my real interest is a little more broad than that. I’m broadly interested in using formal methods to better understand how we use computer systems. I have a long-standing interest in computing education as well as the usability of programming languages tools, and I’m someone who spent a little bit of time, around 2 years, in industry working for Apple, so I’m also particularly interested in the intersection of compilers in programming languages in research and real world compiler hacking.

[00:03:14]
Rachit I’m Rachit. I’m also a second year PhD student in the CAPRA group. I’m broadly interested in using programming languages to understand Computer Systems. I did my undergraduate at UMass Amherst where I worked on Javascript. I have built many compilers which do various sorts of things by exploiting and misusing language abstractions.

At Cornell, I worked on this thing called high-level synthesis which is the idea of taking high-level programs and turning them into hardware accelerators. That’s what I’ve been working on for about a year and a half now.

[00:03:53]
Soham: Great, okay. So, programming languages is the field of computer science that I know the least about. Why don’t you explain to a hypothetical idiot viewer a.k.a me, what programming languages actually is, for someone who’s used one before but doesn’t know what the research field actually entails?

[00:04:13]
Adrian: I think there’s a probably good reason why programming languages seems like an obscure field to you, Soham, because the name doesn’t tell you very much about what it is. It sounds like it should be about inventing new programming languages, the practice of designing a new language. We do that, but it’s actually a tiny fraction of what programming languages people do. So it’s surprisingly hard to describe what we actually do, but it all has to do with how you express..

[pause]

Adrian: … definitely isn’t right. I was going to say how you express your intent to a computer, but a lot of times people do programming language research that has absolutely nothing to do with humans typing code and more has to do with the representation of programs.

So when I think of it, I would probably have to characterize it as all the stuff that has to do with the representation of programs; what computers are capable of doing and combined with that, this very weird theoretical tradition, this formal theoretical tradition that has to do with building up symbolically notions of computation from things like.. traditionally, it looks like algebra I guess.

So there’s this whole area of theoretical programming languages that answers questions like what computers are capable of in a way that is different – from a totally different tradition – from how complexity theorists and algorithms people view it, and that underpins all the stuff we do even when it’s really practical, that view of what computation is.

[00:05:52]
Soham: How would you distinguish that view of what computation is from the complexity theorist view?

[00:05:57]
Adrian: Okay this is in a really cartoonish way, which is that there are two fundamental formalisms for how computers work. The theorists use one - Turing machines. If you’re familiar with Turing machines, they’re like a notional machine that no one actually builds. They were invented by Alan Turing for everything a computer could possibly do. It works by having this magical infinite tape that’s its memory, that reads and writes symbols on it. It has a state transition diagram that tells us what it’s doing.

There’s a different formalism that also represents everything a computer can possibly do called the Lambda Calculus that was invented before computers, that was originally invented to sort of distill down notions of symbolic algebraic reasoning. I think it’s a really surprising fact that those two models of computation are actually equivalent, but everything that we do in programming languages has descended from the latter, from the Lambda Calculus in a certain way, or has some resemblance to this algebraic manipulation stuff as opposed to this state-diagram tapey stuff that theorists do.

[00:07:08]
Soham: Got you. And so, sort of aesthetically different, stylistically different, but fundamentally mathematically equivalent?

[00:07:13]
Adrian: Yeah, mathematically equivalent. I guess the consequence is that programming languages people are usually much more concerned about what programs actually mean, and are much more precise about the meanings of programs and what computers can actually do in the first place, as opposed to, we have almost nothing to say about asymptotic bounds on running time.

[00:07:41]
Soham: I see, which is the bread-and-butter of complexity theory. Excellent! Do either of you have anything to add to that?

[00:07:49]
Alexa: I’d say yes. Another part of the field of programming languages that broadly interests me is also thinking about the fact that there are an increasing number of professionals in the United States and ‘programming languages’, the field, is really closely related to ‘software engineering’, the research field. I was broadly interested in, what are the tools that we need to best be able to explain computation in a very practical way? So I think that’s something really interesting to me about trying to say, okay, there are millions of software engineers in the world. How can we unite this long history of very theoretical tradition of understanding how computation works, to actually align that with what people do on their day-to-day. How do we find a middle ground between what we theoretically want computation to look like, and what computation looks like currently in the hands of software engineers, and unify them to be a better system of programming and computation.

[00:08:41]
Soham: So this is sort of like, usable abstractions for expressing programs in some sense?

[00:08:46]
Alexa: Yes. In that way to me, it’s very closely related to the field of systems, off operating systems and networked systems and like that, and thinking of how we think of abstractions that are actually usable as well as performant.

[00:08:59]
Soham: Rachit, do you have thoughts?

[00:09:01]
Rachit: Yeah. I have a different take on the philosophical musings of PL as a field (I’ll use PL as an acronym for programming languages). So the following statement comes from Matthias Felleisen who is a professor at Northeastern (University in Boston). He has been studying PL for a long time, and he said to me when we were talking about this, “Every application domain comes with an ontology of its own, and ontologies often come with their own languages.” But I think the distilled form of this for PL as a field is that PL people, at least in my eyes, don’t do work in isolation or shouldn’t do work in isolation. They should go to a field, for example, in our group we do architecture and hardware abstractions, so we go into a field and we figure out what the abstractions really mean.

If you have functions, right – people have had functions for a really long time in every language, but the meaning of functions is not well understood and PL people have been trying to formalise functions for a really long time – understanding them allows you to build more powerful abstractions and think about what your programs really mean. I keep saying ‘what programs really mean’ and I really want to stress this point because once you know what programs really mean, you can do all sorts of cool things like verifying the programs and trying to automagically synthesize parts of your program. But to do any of that, you have to understand what your programs mean, and I think that’s what PL people do fundamentally. They go to a field – they can go to networking, they can go to security, or they can go to architecture – and they can pick a language and figure out what the language is actually trying to say and what ideas it tries to capture.

[00:10:48]
Soham: I see. So in a caricatured way, what you’re doing is going to people and saying ‘Ah! I see what you’re doing but there’s a broader organizational principle to what you could be doing that we can demonstrate to you’ which I’m sure makes you very beloved in the fields you [laughs] want to attempt to do this in.

[00:11:09]
Rachit: I think, when you can successfully do it, you can really change fields. I think a lot of, like if you look at the history of computing, it’s a history of languages. When you can really express the languages, you can really express the ideas, and you can build bigger and better stuff quickly. I think you can do it, it’s just hard.

[00:11:29]
Soham: It is very hard.

[00:11:31]
Adrian: I just want to point out that the fact that you got such a long-ended and varied answer to your question, Soham, highlights Rachit’s point that programming languages is, these days at least, mostly defined by its connections to other fields. That is, there are certainly people who do programming languages purely for programming languages’ sake, but I feel like they’re in the minority these days, and there’s a lot more outwardly facing work going on in PL.

[00:11:59]
Soham: I see. It seems like these different conceptions of PL are united by reference to this sort of historical tradition. A lot of sub-fields have evolved like this, but there may not be a single unifying methodological thread necessarily across all of the work. Would you probably agree with this?

[00:12:18]
Adrian: Yeah totally.

[00:012:19]
Soham: That’s interesting. It’s interesting to conceive of what it would look like in a different universe where the history looked different, and his field, software engineering and systems had different boundaries with each other. Okay, so from each of you now, I want to hear what got you interested in programming languages in the first place? A research problem, a paper, or experience, and why you thought that was interesting enough to push you into the field?

[00:12:47]
Alexa: So for me, I took a very roundabout way to coming to this research area, which is that I started college as a Physics Major. I had never programmed, I didn’t have much interest in programming but I took a single CS class and I really liked it. I then went off and did my first bit of research in Computational Physics. I was doing a summer program where I was trying to run simulations of particle depositions, work that was grounded in material science and solid state physics, and tried to model it in a programming language. I was given the option of using Fortran or C at the time, and little 20-year-old me decided to hack on C for the summer.

This was extremely hard. I was doing these kinetic Monte Carlo – which is just a kind of simulation – these giant 2 dimensional C matrices, and found that I just kept getting incoherent results. I would think I was on the right track and then I would realise I had some pointer arithmetic error. So I had this summer of a lot of frustration where I did interesting work and got interesting results but felt fundamentally the tools I was using weren’t very good. This stayed with me when I later took some applied formal logic classes and intro to programming languages at my undergrad institution, realising that there are ways to formally study this as a field, to think about usability of programming tools that we use. I came about it from the sense of having actually taken first this formal logic class at Brown, where I went to an undergrad, called Logic for Hackers at the time, it’s now called Logic for Systems, where you use a lot of different tools to model software at a high level and try to find bugs in your reasoning and implementation. So I came at programming languages from frustrations of usability of existing tools and came at it that way, rather than from a fundamental mathematical background or from a research-first background. I came at it from the side of the applications themselves.

[00:14:45]
Soham: So to a pragmatic ‘How can I use this to improve the thing that was broken for me?’

[00:14:50]
Alexa: Yeah. And then found out that it was actually fun to work on compilers and do the work that’s necessary to realise those theoretical implications.

[00:15:00]
Soham: Rachit?

[00:15:02]
Rachit: I’m going to give a very cheesy answer, which you’re not supposed to do. If you ever want to tell someone why you ever got into a field you’re supposed to give all these very scripted… Anyways, never mind! So, I seriously took up programming when I was in 11th grade. I used to program in C++ ‘98. The details of what C++ looks like are not important here. It’s just like a procedural language. You can write all your pointer manipulating code in there. Then I came to college and I was taking an intro to Java, and I wasn’t particularly enjoying that. Someone recommended I go read this book called ‘Structure and Interpretation of Computer Programs’ which is this really old book from MIT’s introductory (CS) course on this language called Scheme. Scheme is this funky weird language that’s filled with a lot of parenthetical syntax, but the important part with Scheme was that it had something called Higher-order Functions. The idea was that you can write a function that, as an input, takes another function, and it can return functions. The first time I really understood this idea, I remember vividly. I was sitting in some economics class and I was instead coding in Scheme. And the first time I wrote my first higher-order function I was like ‘Wow, this is really cool. I really need to learn more about this.’ Then I reached out to professors and started doing research, and the more I learned about this – and there’s a lot of deep technical work, in-the-weeds work that I did – every time I did something that fundamentally explained a new abstraction to me, I found that to be really cool. That’s what hooked me in the first place, and that’s what keeps me hooked to the field. Every time I can look at a paper, look at an idea, or look at a program and figure out what that program is really doing, I get very excited. That’s why I do PL.

[00:17:10]
Soham: Got you. So your mind was completely blown by these higher-order functions and this was the entry point…

[00:17:15]
Rachit: Totally blown! Okay so, if you write C++ programs, you’re forced into believing that all you can pass in it is data, and data looks like numbers, right? You have numbers and maybe you can put them in some structures, but fundamentally you’re just passing around numbers, and the idea that you can pass these higher-order functions, higher-order ideas that represent some computation and not just data, and the realisation that ‘data and computation are so fundamentally related’ was just mind-blowing. It was such a cool idea. Still exciting till today.

[00:17:53]
Soham: It is a very neat idea.

[00:17:55]
Rachit: Yeah. If you look at modern languages, they’ve all sort of in their own time, 20 years later, adopted this idea – every major language from Javascript to Python, even C++, because it’s such a good idea.

[00:18:11]
Soham: Wait, C++ has higher-order functions?

[00:18:13]
Rachit: It has Lambdas.

[00:18:15]
Soham: Oh, it has Lambdas, sorry. Fascinating!

[00:18:18]
Adrian: C has function pointers.

[00:18:19]
Soham: C does have function pointers.

Alexa: Yeah.

[00:18:20]
Rachit: C has function pointers. But I’m very glad that I didn’t learn of higher-order functions through function pointers because I’d be very angry…

[laughter]

Rachit: …as I was when I learned about function pointers.

[00:18:30]
Soham: I messed around with function pointers in high school, it wasn’t fun!

[laughter]

[00:18:36]
Soham: Would not recommend!

Rachit: Whoops!

[giggles]

[00:18:40]
Soham: Okay Adrian, what about you?

[00:18:41]
Adrian: I started grad school trying to decide between two different sub-fields of CS - computer architecture and theory. I’d done theory, algorithms stuff - algorithms for optical networking - in undergrad, and I thought that would be pretty cool, but it turns out I’m very very bad at theory. I tried doing it and I’m super glad that I don’t do that! I’m glad there are people in the world who are actually good at it I guess…

[laughter]

Adrian: …who are not me! I was sort of simultaneously discovering that and also trying to get started on architecture research. I was talking to my advisor, and – I think it’s fairly standard – my advisor thought with this new grad student, he asked me ‘which of several ongoing projects would I like to try getting involved in?’ I decided one that would sound super cool was one that was addressing this fundamental tension in computer architecture, which is the difference in parallel processors between message-passing and shared memory, that you can either have machines that have access to one big memory and they all communicate through that, or they actively send messages to each other and receive those messages to communicate. They have a fundamental set of trade-offs but all the real machines that we use today are all shared memory machines. The multi-cores all have the one gigantic main memory. So the idea was, maybe we can remove some of the sharp edges that everyone knows about the program ability of those machines, that is you accidentally write something that someone else was using in that shared memory by restricting who can read and write shared variables after the last person who read and wrote it. So you’re sort of restricting the communication through shared memory in a message-passing style, and this seemed really interesting to me. It had a nice formal graph processing properties that seemed cool to me, and as we got deeper and deeper into it I realised that what we were actually doing was designing a set of annotations to Java and a one-time checker that gave you exceptions when you violated the policies that you’d written down, which is definitely programming languages research.

Ed note: Adrian is talking about his 2010 OOPSLA paper Composable specifications for structured shared-memory communication. Full text of the paper available here.

So by accident, I ended up doing programming languages research in order to solve what I thought of, as a first year grad student, as an architecture problem. To look back on it, I now do actually believe that programming languages is the right way to solve architecture problems. I came out originally from thinking that all these problems, building and defining what a computer is from the silicon up seemed really cool. But there are not many interesting problems that are solved just at the level of designing processors, just fiddling around with gates, or trying to make existing ways that we build computers a little bit faster. All the interesting problems have to do with looking up the system stack to make things more programmable or getting collaboration from the compiler, for example. All that stuff has so much more to be done than the traditional areas of computer architecture that are locked in their own abstraction level. No offence to anybody who does that kind of research! Again, I’m glad there are people who do that, but I think it’s way more interesting and there’s a lot more potential to change the world with this sort of multi-level view on how hardware works.

[00:22:01]
Soham: Is this because a lot of the fundamental hardware work happens in industries? Like, you can’t really do chip design in academia (anymore)?

[00:22:12]
Adrian: I think that is definitely part of the reason. Modern CPUs, for example, are so wildly complex, that you can’t possibly say whether your branch predictor is better or worse than Intel’s branch predictor because you have no idea how Intel’s branch predictor works. But I think even in a situation where everything were open source and we could inspect them, I still think that traditional architecture work that does not attempt to do some sort of programming languages or compiler stuff is tying itself to a legacy that comes from the 60s in terms of the way that we design the interface to processor. It is fundamentally trying to say ‘we’re building this machine that runs instructions one after the other or at least appears to, and we’ll just try to take that thing and make it incrementally better.’ That approach is fundamentally limited. It’s like you are hiding behind an abstraction boundary that can only get you so far. That is how architecture has worked up until about 10 years or so ago, but suddenly things are beginning to shift, and we have the chance to actually change how things look and work in the hardware, as opposed to just changing things underneath that abstraction level.

[00:23:23]
Soham: That makes sense. Actually continuing out from this, can you talk about a recent research problem that illustrates what you mean here, that you’ve worked on?

[00:23:32]
Adrian: How recent do you want?

[00:23:36]
Soham: More recent than your PhD maybe? But not necessarily in the last 25 minutes.

[00:23:44]
Adrian: Sure, yeah! Can we talk about Dahlia stuff, Rachit – is that okay?

Ed note: he’s talking about Rachit’s Dahlia paper from PLDI 2020: Predictable Accelerator Design with Time-Sensitive Affine types.

Rachit: Yeah.

[00:23:50]
Adrian: Cool. Okay. So, one thing we’ve been working on in the lab a lot lately is using a Programming Languages view on generating specialised hardware for particular applications. The motivation being that this traditional approach to designing hardware that I’ve been talking about - which is you use a standard instruction set to express your program and then hope it goes pretty fast - has fundamental limitations, in part because it is trying to do everything with a single piece of hardware. There is a sea change in the way that computers are built going on right now – it has to do with the designing of special focused hardware that can do individual tasks far more efficiently than a general purpose processor can do them. So there are great stores of efficiency to be unlocked if we had the ability to generate specialised hardware accelerators for many new domains.

Unfortunately, this is ridiculously difficult to do with current programming tools. The languages people use to design hardware at many different levels of abstractions are all… If you are a programmer, you wouldn’t even recognize these languages or these compilers. They are so incredibly difficult to use, and the compilers are so proprietary and buggy, that they are a huge impediment to getting anything done in the area of designing hardware accelerators. So, our notion is that it might be nice if we could design specialised hardware and reconfigurable hardware in a way that more resembled ordinary software development. If we had languages and tools that actually worked and produced the results you thought you would get from the source level, then we could unlock the potential of millions of human designers to build hardware accelerators that the tools currently prevent them from doing. Is that a fair summary, Rachit?

[00:25:49]
Rachit: Yes.

[00:25:52]
Soham: That’s really cool. So when you talk about these hardware design languages, you’re talking about FPGA stuff, or VHDL, or something like this?

[00:26:00]
Adrian: Yeah. FPGAs are Field-Programmable Gate Arrays which are a kind of reconfigurable hardware. They are actually a nice way to get to the properties of hardware specialisation without paying the, like, millions and millions of dollars that it would cost to manufacture actual silicon.

Soham: Right.

[00:26:17]
Adrian: So, a lot of our research currently focuses on using those as a general purpose compute unit; having programming languages that are hopefully higher level than VHDL which you mentioned, to express what you want and how you want to compute it on an FPGA.

[00:26:35]
Soham: So currently you’re competing with things like VHDL that do, roughly speaking, work at the gate level or with slightly higher level than gates but not all that much?

[00:26:43]
Adrian: Yes, that’s right. The other thing that we’re competing with is a very strange notion that some people had a couple of decades ago, to compile C to languages like VHDL that work at the gate level. That is, to take in – according to them – arbitrary C programs and try really really hard to generate a good accelerator. It is perhaps not surprising that these compilers, which are called high-level synthesis or HLS compilers, which Rachit mentioned a bit ago; these existing compilers don’t work, they don’t do what I just said. They don’t take arbitrary C programs and generate good accelerators. They take a funky, ad hoc, weird subset of C that sometimes works and compile it occasionally to an accelerator that might or might not be good.

[00:27:26]
Soham: Occasionally as in, it’s not deterministic whether it compiles at all?

[00:27:30]
Adrian: Well, not deterministic is a little too far. Depending on the… Let’s put it this way: small changes in the input program could cause, and do cause, these compilers to reject your program or to generate very bad hardware.

Soham: I see.

[00:27:46]
Adrian: So, I think it’s totally unsurprising that if you try to repurpose a language which is designed for CPUs several decades ago, and repurpose it as something for generating accelerators, they would not work as well as it does for a CPU.

[00:28:00]
Soham: Is there some kind of heuristic-based translation to hardware design?

[00:28:03]
Adrian: Yeah, you got it. It’s totally a big pile of heuristics that tries to guess what the program, how it might map onto hardware and generate an architecture that looks like that.

[00:28:13]
Soham: Seems somewhat wrong-headed.

[00:28:14]
Adrian: It is, like I don’t blame people, you know?

[laughter]

Adrian: But it is an obvious mismatch for where we are today. It might have made sense a few years ago to say ‘yes, let’s take legacy software and compile it to good accelerators’, but I think it’s clear that it doesn’t make sense.

[00:28:30]
Soham: Ah! I see, so that’s what the notion was. The notion was you wouldn’t have to rewrite it. You’d just take some pre-existing (software)… Yeah…

[00:28:33]
Adrian: …maybe like sprinkle in a few annotations here and there, and then get a pretty good accelerator. But, I think it’s clear from the modern perspective that it’s not the right way to go, but that the dream of having some sort of higher-level way to write down, or let competent software programmers design hardware, that shouldn’t be dead. We should abandon the idea of compiling legacy software, obviously. But there’s something to be done in the design of languages and compilers to make it more accessible.

[00:29:02]
Soham: Got you. So, Rachit, are you working on this project?

[00:29:06]
Rachit: Yeah. I worked on this project as well. Do you want me to talk about it?

[00:29:13]
Soham: Yeah. Can you talk about how, what you’re actually doing to build this thing? What is it that you’re actually building?

[00:29:21]
Rachit: Yeah. So before I talk about that, I’m going to add a bit about why I think the problems occur from a more detailed level, and then maybe I can talk about what we’re going to do to solve the problems.

[00:29:34]
Soham: Go ahead.

[00:29:35]
Rachit: I think there’s a general trend of what you see with a language that’s hard to program, or how unpredictable behaviour doesn’t really make sense when you compile them down to a target. There’s this notion of something called the semantic gap in programming languages literature, which is the idea that you’re compiling from a language A to some language B; language B could be representing some sort of hardware or some sort of virtual machine. When the gap between these two languages is big, it becomes really hard to reason about the behaviour of your programs when you write a program in some target source level language A and then compile it to a language B.

[00:30:18]
Soham: Can you give me an A and B, some languages people would know where the gap would be large?

[00:30:23]
Rachit: So, a canonical example of this is you write C++ code and it turns into, say, x86 Assembly that’s then executed by the processor array. So Assembly and C are surprisingly very close, when they were built first, surprisingly very close to each other. They were like a thin wrapper layer on top of Assembly that gave some set of nice structure programming primitives, but it was really meant to be at the lower-level Assembly programming language. So the semantic gap between C and Assembly is not very high.

Now on the other hand, you sort of ran into this problem that your primitives in the language are very low-level. C famously has pointers, and pointers famously have a lot of bugs, because programming with them is hard for some definition of hard and some definition of who programs them. So people have rolled other languages. Another example is Java which compiles to the JVM or the Java Virtual Machine. The Java Virtual Machine itself has its own instruction set called the Java bytecode. The Java bytecode is again higher-level than Assembly, but lower-level than Java. So, if you think about programs and computers, there’s this giant hierarchy of languages in the middle, and when you’re jumping between this hierarchy - when you’re going from a higher level to a lower level - if your gap is too big, you’re going to run into problems with the programmability, predictably and understandability of your programs.

[00:32:01]
Soham: So you’d say that Java and x86 Assembly have a big semantic gap?

[hesitates]

[00:32:06]
Rachit: Yeah, I would say that. Java has things like virtual dispatch, which you have to compile a lot of code to them. You have to build up a lot of runtime support and you have to compile a bunch of code to make that a reality for something like Assembly which really doesn’t have virtual dispatch. It’s like an idea of dynamically selecting the right object to execute some piece of code on. Assembly doesn’t even know what objects are, much less what selecting the right object means, right? So the semantic gap is high. But it’s nowhere close to high-level synthesis as the semantic gap between high-level synthesis in the problem of synthesizing a higher-level programming language and to lower level hardware it’s much higher because, you’re trying to take some program that represents a computation and you want to compile it down to a computer, right? You want to take some physical notion of resources and you want to use that as a basis for implementing your computer? This is a totally wild idea. Everytime you write a +, it doesn’t mean an instruction execution like it usually does in a programming language. It means ‘build me a physical adder that’s connected to my inputs and then returns a result to my output.’ The expression A = B + C is a physical circuit that you need to think about. The way we’re looking at it, and the reason this is really hard to reason about, and the reason there’s so much complexity when you compile computations down to computers is because you don’t reason about the physical resources. You don’t think of the + as a physical resource, and that’s what causes it to be really complicated.

If you had some notion of your physical circuits being physical, real and usable in your code, then maybe you can reason about it. But again, if you go too low-level you end up with something like Verilog, where yes, you do get real physical resources, right? You can build an adder and you can connect wires to it. Then you can execute your circuit in it. But if you go at that level of granularity, you can lose all your abstraction benefits. Then you’re just programming at a lower level. So there’s this interplay that’s central to field research, at least the kinds of research we do, where you have to trade off expressiveness for some sort of notion of capturing the semantic gap. Does that make sense?

[00:34:43]
Soham: Sure.

[00:34:46]
Rachit: Yeah. So, the way we’re trying to solve this problem is using fancy typesystems. If you come from a traditional programming language background, if you program in Java or C++, you don’t really think a lot about types. You sort of look at them and you’re like ‘okay I have a type that says I’m an animal, and this is a dog, and I can replace all instances of animals with dogs’. This is like a canonical inheritance-based typing system in something like Java. That’s usually straightforward to think about but there’s more complexity that you can add in your type system to capture more ideas about the language you’re working on. So for example, Rust is a new systems programming language that has been recently very successful in building what are called Safe Systems Programming. It’s been enabling people to write some very complicated systems code that is concurrent and uses memory in very fine-grained ways and yet manages to be safe. Rust accomplishes this with a culmination of good language design - just good primitives and good design decisions - in conjunction to having an interesting type system that captures some semantic notion of your program. For example, one thing the Rust type system tries to guarantee is that, if you have pointers to memory, you’re never in a state where you have multiple pointers pointing to some memory, and then all of them are trying to mutate that memory. Rust hypothesizes that’s one of the biggest causes of unsafe memory bugs. To some large extent, this has been true because people using Rust have been able to build really big software like Firefox’s rendering engine using Rust, and using mostly safe subsets of Rust. The higher-level point being, you can use typesystems to capture properties about your program. So we’re sort of taking this approach, we’re using a type system to capture physical resources as an idea in hardware programming but we’re doing it at a level of C or C++, or even higher.

[00:37:04]
Soham: So the resources here are like, an adder would be a resource, for example?

[00:37:09]
Rachit: Right, so when you write your program ‘A + B’, + is a physical resource. + would be given a type that says it’s a resource. This is important because when you build circuits, one way to build circuits, if you come from a background where you, like a naive way to build circuits, would be, everytime you build an adder you just connect it. Like every time you want to do A + B you just build a new adder, right? And you can build a really massive circuit that can do all of the computation in one go but takes all of the area on your FPJ or all of the area on your silicon.

A more common and more interesting way of building circuits is, you have some number of adders that are available to use. Let’s say you have five adders and you want to do 100,000 adds, and you want to use only five adders to do it. So, you do this thing where you try to use as many adders as possible in a given timestamp, and then when you want to use more adders you finish your computation at that point, save it into some memory and move on to the next timestamp. Now you have five more resources to use again. This is something called time multiplexing where you have a fixed number of resources and you want to use them to do more computation than they would allow in a single timestamp. You multiplex them over time. You reuse them over time. That’s how you get to do big computations with a fewer number, like a few resources.

[00:38:44]
Soham: I see. So you want to enforce, you want to, in your type system, express that something like this - multiplexing can be possible while ensuring that you’re not using more resources than you have - or something like this?

[00:38:58]
Rachit: Exactly. That’s precisely what we want to do.

[00:39:01]
Soham: I see. That makes a lot of sense. Is the approach to this project that you sort of sit down, you think about this from a more top-down perspective like ‘I have this problem’ and you design a type system to make it work? And then you sit down and crank out the details of the type system in theory and then you implement it?

[00:39:16]
Rachit: Yeah. That’s the fun part of research. You can have simple notions of what and how each project will go but then they don’t really go like that! So usually in essence, the way it works is that there are periods when we think really hard about the things we want to express, and then there are periods when I’m just cranking out a lot of code. We switch between these. There’s no sort of clean separation between the time when we’re thinking and the time when we’re building because we think of something, we build something, then we run some experiments, or we write some code, and try to figure out ‘can we actually express the properties we want to express in programs in a reasonable way’. If we realise we can’t or if we find it a bug, or if we find that we have mistakes in our reasoning, we go back to the drawing board and we build it again.

So there’s a lot of iteration going on, fundamentally sort of a design trade-off. You’re designing something that is expressive and safe. These are two competing forces. You can have something that’s safe by just rejecting every program, and you can have something that’s expressive by accepting all programs, and you don’t want either of those to end. So, you’re trying to find a design point that allows you to express as many programs as you can while also keeping the programs you write safe. Safe here is sort of a technical term in the PL world where safety means you’re capturing some property of the program wherein you’re saying every time I typecheck, I can prove safety, which means I can prove this property holds true for your program.

[00:40:49]
Adrian: Just for fun, I think it would be nice if our minds were organized enough that we could do it, you said, and sit down and figure out all the theory, and then take that into an implementation and be done with it. Like Rachit says, it is in reality a wild flip-flop back and forth between those two modes, which I think is pretty fun. At least this way I don’t get bored I guess, with the thinking and the doing happening all at once. But, I think it is really true that in research projects that at least I have done, I have not really figured out what we are actually making until we have mostly made it. So it would be really hard to figure that all out upfront and then take our dreams and turn them into a reality all at once.

[00:41:45]
Alexa: I would argue though, that even in an ideal world, I wouldn’t necessarily want this intense separation between all the theory and the thinking first, and then just all the implementation. I think that you know a problem is important if you run into it yourself to some extent? So doing all the thinking ahead of time can mean you’re not actually solving the right problems. That sort of the advice I had gotten from an undergrad advisor was that, go off and do industry for a while, or actually embed yourself a little more in communities of programmers and figure out what are the things that people find difficult and you use that to inform what you do. I think that’s kind of true for research too. Even if you have a really beautiful theoretic idea, I, at least, am actually motivated by seeing - how does it feel when you actually try to implement it and play with it? What are the challenges there? And then use that help to also figure out what theory you need next to support that.

[00:42:39]
Soham: Adrian, can you describe one instance of this kind of back and forth, where you have theory, and then you implemented it, and then it broke, and then you went back?

[long pause]

[00:42:52]
Adrian: Give me a second, that’s interesting.

[pause]

[00:43:00]
Adrian: Yeah. I feel like this happened about 10,000 times in this very project that we’re talking about, where we had a very simple notion of the theory for this language. So for the typesystem we’re going to develop, but the main problem was that it was too restrictive. Like Rachit was saying, it is always safe to reject every program, and we were rejecting most programs. So, we would sit down and like, take that theory, make a very very simple checker that implemented that theory that we had in mind. And then, to absolutely nobody’s surprise, no useful programs could be written in that language. The point was, we had to go back and say ‘oh we really want to allow this specific thing, that it must be programmed to be able to do this’ which is obviously okay, but our type checker can’t currently certify it.

[00:43:49]
Soham: What’s an example of the ‘this’ that you wanted it to be able to do that it couldn’t?

[00:43:54]
Adrian: Okay, it’s a little hard to get into this without getting very detailed about our type system, but one thing that we needed to be able to allow… Okay, one thing we needed to be able to prevent is that an accelerator that we generate tries to write two things into the same place in the same memory at the same time.

Soham: You wanted to prevent this?

[00:44:14]
Adrian: We wanted to prevent that. Exactly. So, we had something that ruled that out. However, we discovered that it would be actually kind of cool if programs were able to read the same place in the same memory at the same time, which sounds very similar, but is totally different because it’s absolutely fine for a circuit to get one value out of the memory and just split it to copy it, and send it to two different places and use it in two different computations.

[00:44:42]
Soham: Right. You can imagine doing some pre-computation and then having a bunch of different, other parts of the circuits read it to do some further computation on it that’s distinct.

[00:44:49]
Adrian: Exactly, yeah, right. A simple version of our type system would rule out both of them. It would say ‘you can’t touch memories at the same time from two different places.’

[00:44:58]
Soham: Right.

[00:44:59]
Adrian: But it turns out we actually had to discriminate between reads and writes to make sure that this was allowed to do simultaneous reads.

[00:45:04]
Soham: Got you. And this probably introduced additional complexity into the type system which you had to do because you wanted these to be useful programs?

[00:45:10]
Adrian: Exactly. Our whole thing is totally worthless if we can’t write useful programs.

[00:45:14]
Soham: Right. That’s really fascinating. There’s a similar back and forth that happens with systems research. Unless you’re Leslie Lamport, a lot of practical systems research doesn’t start with a lot of theory. It starts with these notional heuristics of what we think is possible, and then some specific pieces of theory like consensus or something like this, that act as constraints against what we can and cannot do. There’s a lot of relaxation of the models we have. Say, like, ‘Oh! we can’t provide linearizability, or strict serializability’ which is a very clear notion of all events in a database happening sequentially with respect to each other. But we can provide this slightly lower property or this lower isolation level to this particular thing.

So it seems very similar in that sense, also in the sense of developing this right abstraction, this sort of Goldilocks abstraction that you want, that is powerful enough but also not too powerful that it’s just misusable by your median programmer, while also being implementable in performance. It seems like these are two sides of the same coin. In this vein, for any of you, what do you think are the distinctions between doing PL research like this, and doing systems research like this? Why would you do one or the other?

[00:46:35]
Rachit: Can I jump in?

Soham: Of course.

[00:46:38]
Rachit: Okay. This is a very interesting question about PL as a field. And this is something I think people in our position struggle with a lot, because to me PL is a field that straddles between theory and systems, right? I did and I do identify as someone who does systems and PL together. I don’t do PL in isolation. I do PL for systems of some form. But it means different things to different people. I also have friends that do very pure, from my point of view, theoretical work, that is just about building really clean, really theoretically strong foundations for PL research. Then there’s people I know who work on memory allocators, for example, who work on building really nitty-gritty systems. I call all of these people PL people because the unifying step between all of them is they’re thinking about languages. They’re thinking about abstractions and that’s the loose definition of PL I work with, which ends up with me classifying a lot of systems work as systems PL-adjacent work anyways. I don’t know if people in the PL community who’ve actually been in the community for a long time or a longer time than me would agree with this, but this is one useful way of thinking about PL, because I do think it’s this field that sits in the middle. It thinks about abstractions and tools for building abstractions and without a field, it’s not very useful to think about PL, without another field to apply PL to.

I also think most fields can benefit with the ideas from PL. So, there’s this nice interplay where if you really enjoy doing some research and you learn about some ideas from PL, you can probably apply them in your field and build something cool.

[00:48:31]
Soham: So Alexa, earlier you were talking earlier about this notion of usability, right? And there is this tension, at least as an observer, in programming languages where a lot of arguments that people make in the introduction to their papers are about usability and about how this is sort of more due to abstraction; it’s cleaner, and produces less areas and so on. Well in practice, there’s not a lot of empirical work actually measuring whether this is true with real programmers. So is this changing? What do you think is the future of doing research and actual usability in programming languages?

[00:49:03]
Alexa: Yeah. I think I’m quite new to the community overall. I’ve been in the PhD program for only about a year and a half. I think my perspective from having read a lot about, and talked to people who’ve been into the field for longer is that, the tides are changing in this and there is a broadening interest in the intersection of programming languages and the field of human-computer interaction. So HCI is the independent tradition of how we understand how people use technology in a very user-centric way which sounds kind of repetitive, but understanding if you build a new interface, does it actually operate, and are people’s mental models of that interface aligned with what you intend them to be?

Traditionally, this is done with interfaces that don’t exactly look like programming languages but I would argue, and I think a lot of people are arguing, that every programming language is an interface and if you want to make a really strong claim about how usable your tool is, it would be good to actually - maybe not in every case - do a user study, but have some way to demonstrate this usability more empirically. There are workshops now that are at the intersection of PL and HCI, people have gotten NSF career awards that are focusing on this intersection, and I think there is more of a push to say if your paper’s going to claim something really strong about usability, you better at least have some data to back it up. This can really range. I’ve seen papers that say ‘Oh, we think our tool is usable because we had a grad student try to do it the old way and it was slow, and then they used our fancy new tool and it was fast’ and I’d say that’s a really low bar for doing anything usability-oriented, but at least is saying, trying to have some idea of how people are ultimately going to use this. And is it necessarily the case that a particular research team finds something more usable or cleaner? Do you actually know that’s true for the intended end programmer in the situation? I think you need actual data to back that up rather than just saying ‘we think this is the best’.

[00:50:58]
Soham: Is there a specific trajectory you see for how the field might best progress in this way? Is there a set of guidelines you can see in your mind for what you should do if you’re starting a PL project that has a human interface component?

[00:51:13]
Alexa: That’s a good question. I’m not sure I have an exact answer there. In the same way how we’ve talked about how it’s not a precise cycle, how you go between theory and implementation, I also don’t think there’s a precise silver bullet to understanding theory to implementation to usability. I think trying to learn from the HCI community, for example, one thing I’ve learned through taking classes and talking to people is that there really is a big difference between two types of user studies you can do. You can do what’s called a summative study, which is maybe what you think of as - you give people a tool, you ask them to engage with it and then you actually measure - could people do the tasks you wanted? Did people understand what they’re doing? Did they rate the experience highly? That assumes you have a finished system and you have people who are able to use that system in isolation and treat it as a black box. What you can learn from the HCI community is that’s not the only way forward. You can do studies that are more formative, that are more need-finding-based, where you find a body of users and as we’ve been saying, PL is all about intersections. You find a group of users who are actually at the other side of the intersection, who are ingrained in the domain you want to study, and you ask them what they need, you ask them to give their perspective on your high-level ideas before the system is actually designed, and have them play with a prototype you don’t assume is completely done. You don’t need an ‘n’ for these studies to show your massive statistical significance. You need a smaller group of people who can actually inform their perspective on the domain that you might not have. I’d say that’s recognizing that user studies don’t need to be massive to the extent of black boxes, but can actually be ongoing with the project as it develops.

[00:52:57]
Adrian: Yes, I think that’s exactly right. Like Alexa says, I think in terms of designing studies for usability, most of the answers can be found in HCI. The HCI community has worked really hard to develop methodologies and best practices for how to run studies by usability. This should work just fine for programmers as they do for non-programming HCI questions. I think a big thing the community will have to address as it embraces this further is finding ways to determine when is the right time to do your study, and what the right questions are to ask when interacting with real people. So I think there’s so many ways in which it would be possible to ask bad research questions and then turn them into your studies that don’t give you a meaningful result. Some of them are really important questions. For example, I think it would be a really bad idea to try to do many more user studies on the question of whether statically or dynamically typed languages make programmers more productive, which in some sense is a really important question. Programmer productivity, you can argue, is a really important thing, and this is a difficult question to answer. I think it is too diffuse of a question to answer all by itself. There’s so many different levels of experience of programmers, there’re so many different things that programmers want to accomplish, and there’s so many differences between languages that are statically and dynamically typed that conflate that question, that make asking that thing precisely all by itself, is not a really good thing to get a bunch of funding and do a user study about. What we need to do is develop a better science for how to take these big broad difficult questions and distill them into things that empirical methods interacting with humans can actually answer.

[00:54:45]
Soham: Yes, and this is a hard problem in all social science allied disciplines; finding these nice questions where you don’t have confounders that destroy the chance that you get any useful data. What you’re saying suggests that there’s a good opportunity to do good social science work in programming languages, to work at the intersection of these things. Not to throw any shade at the HCI community, I don’t know if they themselves are doing sufficiently methodologically principled empirical work. I wonder then if it makes much more sense to import things from behavioural economics and other disciplines that have more replicated work with large numbers of people. It’s hard to get large numbers of people to do HCI or PL studies, especially PL where you need people with some level of experience as you were saying earlier. It seems like a difficult question, but I certainly hope there’s some progress on it. So, switching gears a little bit. I want to ask each of you to highlight a piece of research that you’ve seen at any point in your career - it can be as old as you want it to be or as new as you want it to be - that you think this is interesting and successful at what it wants to do, in PL.

[00:55:57]
Adrian: Sure. I have an example. I think it’s going to sound like a cliche to both Rachit and Alexa, but I have this paper that I really love that changed the course of an area in systems and programming languages. It’s a paper by Hans Boehm titled ‘Threads cannot be implemented as a Library’ (Ed note: in PLDI 2005) which is fun not just because it has a really intriguing title that sounds like it can’t possibly be true, but also because it launched an area of investigation that is both beautiful and important. The thesis of the paper is if you take a normal programming language and you try to make it multi-threaded by adding on what looks like a set of library calls, like create a thread and synchronize with this thread and destroy a thread, for example, that can’t possibly work because the compiler will make assumptions that those are normal function calls even if they are black box function calls that can cause it to do optimizations that will break your program. CPUs, similarly, will see those as normal functions calls and do things that are illegal in the context of the multi-threaded program. They’re just fine in the context of the single-threaded program.

Soham: What can they do?

[00:57:07]
Adrian: They can introduce non-determinism into a program that is perfectly deterministic. They can optimize your program to add writes in where programs never did writes and turn that into something where two different threads are trying to read and write the same variable without synchronization. This can cause a program to do arbitrarily bad things. The lesson of the paper is, it’s not sufficient to just bolt this on to existing languages. It is fundamentally necessary for compilers and the semantics of languages to change in order to support any sort of shared memory multi-threading. It launched an area of research into memory consistency models that is still with us today, where we’re trying to figure out what multi-threaded programs even mean at the level of source languages and ISAs.

[00:57:59]
Soham: Fascinating. When was this published?

[00:58:01]
Adrian: This was in the 90s or early 2000s. Something around there.

[00:58:06]
Soham: Was it true that, at the time, people were bolting on threading libraries to existing languages?

[00:58:12]
Adrian: It’s absolutely true. In this paper, it’s not just a theoretical worry. There were actually compilers out there trying to do exactly this thing, and you could demonstrate actually wrong results.

[00:58:21]
Soham: And now people don’t do this as much? Now people build threading into the language model?

[00:58:25]
Adrian: In part. Hans got onto the C standards bodies and the new C standards as of 2011 actually give us semantics that has to deal with threads.

[00:58:35]
Soham: Wonderful! That seems like a wonderful encapsulation of lots of pieces of this. Rachit, do you have one?

[00:58:42]
Rachit: Yes. I was trying to think of a way to explain it. There’s this paper from the early 2000s, and the paper has two titles - the first title is ‘Languages as high-level operating systems’ or something like that. But the title I remember is ‘The Revenge of the Son of the Lisp Machine’,which is a very cool title for a paper. I think people should title their papers like this.

Ed note: the paper Rachit is referring to is Flatt et. al.’s Programming Languages as Operating Systems from ICFP 1999.

[00:59:13]
Soham: What was the title, say it again?

[00:59:15]
Rachit: The Revenge of the Son of the Lisp Machine. Following the tradition of some movies that are titled ‘The Revenge of blah-blah-blah’. The highlightable point of the paper, to summarize this in one statement is - Languages and language systems can provide primitives that you usually think of implementing through operating systems. So, one common thing that your operating system does when you’re writing a program is provide process-level isolation. It guarantees that one process doesn’t try to destroy the integrity of another process that’s also scheduled in your operating system. The central investigation of this paper was trying to figure out, can we build a language that provides these guarantees at a language level, so we can reason about these abstractions at the language. I found this paper to be really cool because they managed to build all of these things that we traditionally think of as operating systems abstractions into a language. So they have language level sandboxing, language level threading, similar to what the paper Adrian was talking about. You can’t just have threads implemented on top of a compiler as a library. You have to think about it inside the language and they’ve tried to do that. They have this really cool evaluation where they take their programming environment called ‘Dr. Racket’ – all of this was implemented in the language called Racket which is a descendant of the Lisp programming languages – They took Dr. Racket and they started Dr. Racket inside Dr. Racket to show that it had sandboxing capabilities. Then they took the sandboxed version and started another instance of Dr. Racket. So they had triply nested Dr. Racket, and they showed that you can kill threads in the most-nested Dr. Racket and it wouldn’t affect any of the other Dr. Rackets. They also found cool bugs in the compiler and the sandboxing system where they were unable to show ‘you can’t discover this bug unless you go into the third level of the hierarchy.’

Ed note: Racket and the aforementioned Scheme are very similar.

The paper is also written in this interesting way where there are experience reports. This paper wasn’t written in one go, it wasn’t just a year-round project. It had been going on for several years at that point. The paper was written in this funny way where you have normal technical prose, and then you have these experience report black boxes where they talk about how they came to design decisions. There’s this really nice interplay. When you read a technical paper, it’s written in a way to make the reader believe the author is an amazing genius who came to the right abstraction every time. If you read that paper, it’s really nice because you can see how they came to design decisions when they were building these things. It’s a cool paper and it has some cool ideas. There was some other related work in the systems community maybe before or around the same time called the Synthesis Operating System, which was trying to do similar things and provide isolation guarantees. I think isolation guarantees is what that code overwrites in the operating system, I might be wrong. That’s a really cool paper. It’s a good technical piece of writing and it’s also good study on how to write PL papers.

[01:02:41]
Soham: Nice. Alexa, do you have one?

[01:02:42]
Alexa: Yes. I’m going to go on with my theme. I’m not going to give a single paper but actually talk about a tool that got me interested in the field of formal methods, and then some papers that went along with it. The tool is called Alloy and it’s both a specification language, and it comes with a graphic interface called the Alloy Analyzer. It was started at MIT by Daniel Jackson’s software abstraction group in the late 90s. It came to prominence more in the 2000s. The basic idea of this tool is to be able to model software systems as operations on sets. So the language itself is super small, the grammar fits on about a page, and you model your system as a series of sets in relations on the world. It’s very simple to do things like, to model changes in your system you actually model specifically states of the world and then describe transitions between them. It has this nice clean syntax. What the system does underneath is, there’s an implementation called Kodkod that translates really high level descriptions based on a set-theoretic notation down into a SAT Solver. If you’re familiar with the SAT problem, that’s just Boolean satisfiability – can a given boolean formula be satisfied. What I think is super cool about Alloy is that it was intended to take the idea of formal methods, the idea of using solvers and proof systems, and make it more applied and more lightweight and approachable by bounding it.

Ed note: The Princeton paper is Caroline Trippel’s 2018 MICRO-51 paper CheckMate: Automated Synthesis of Hardware Exploits and Security Litmus Tests.

So, Alloy works as a bounded solver, it only solves instances up to a certain size. It can’t prove things for all. What’s interesting about it is, since the early 2000s when it came out, it’s been used in a really wide array of systems. There’s some recent work from maybe 2017 out of Princeton - using Alloy to find bugs similar to Spectre and Meltdown - the speculative execution bugs by modelling really small memory models. There’s been lots of work in this flavour of thing. It’s based on the small scope hypothesis which is basically - if there are bugs in your program, you can probably find them with pretty small instances rather than giant instances. There was another paper in 2015 from the Alloy group itself extending Alloy to be able to do more complicated, higher order constraint-solving. Now there’s thousands of papers using this tool to show that, even though it’s quite small, you can find lots of bugs by abstracting your system in a way into this language and then running a bounded analysis on it using a solver.

[01:05:18]
Soham: That’s really cool. What’s an example of a simple thing you could prove in Alloy?

[01:05:21]
Alexa: The interesting thing with Alloy is that you’re oftentimes not really proving anything. Unlike SMT solvers or SMT (Satisfiability Modulo Theories) the most common of which is Z3 out of Microsoft research, where they actually are theorem provers, you can actually say definitely something is true. Alloy isn’t really about proofs, it’s about modelling a system and being able to find things inconsistent. A really famous example that intersects more with your field of systems, is there’s this protocol called Chord for distributed systems where you have a bunch of nodes and a ring, and you want to be able to say things about communication in this ring. This system stood as presumed correct for decades, I think about 20 years, and then a researcher was able to find that in certain pathological cases, the Chord protocol could actually break into two disjoint rings that never come back together. She did this using Alloy. That’s an example of something that she couldn’t necessarily prove that it was always correct for all sizes, but what she could prove was that it was incorrect in one particular case that was a real world case that led to changes in the protocol to fix this.

[01:06:24]
Soham: So Alloy lets you model a system and then you can sort of poke it with a stick and…

[01:06:29]
Alexa: Exactly! Poke it with a stick and then find where the facts that you think should be true about the system aren’t true. You can also do bounded verification and say ‘up to this size of instance, we do know that exhaustively, there are no issues.’

[01:06:44]
Adrian: You could say you poke it 10 million sticks fairly quickly.

[01:06:46]
Alexa: Yeah.

[01:06:49]
Soham: That is very neat! Last question for each of you. What is an area of PL that you think there’s a lot of opportunity for people to do future research in, and what’s your 30 second pitch for why people should work in PL in particular?

Alexa: Haa!

Soham: Alexa, let’s start with you.

Rachit: Can you repeat that question, please?

[01:07:13]
Soham: Yeah. The question was - 1. What is an area of PL or some research topic that you think there’s a lot of opportunity for people to do research on in the future, that you would like to see more work on? 2. What’s your 30 second pitch for why people should work in PL in particular if they’re gonna do work in computer science?

[01:07:30]
Alexa: I’ll go first. My area maybe is a little hypocritical because I’m not myself working exactly in it, but I think what we talked about earlier, about usability in PL is super important. There’s bounds and leaps to be made in terms of the methodology we have for conducting user studies on programming languages and programming languages tools like compilers. I really hope there is even more, except there’s a kind of sea change there. But, I hope that continues and there’s a lot more work. I specifically hope there’s more work at this three-way intersection of programming languages, systems and hardware, and usability. Just because something is deeply technical and requires complex abstractions at the systems level, doesn’t mean we shouldn’t care about usability in that domain. 30 second pitch for PL is - Something I think that’s really cool about it is, it touches every single researcher who does computing research. Even the theoreticians probably at some point write some simulations or enaction of what they’re trying to do. It’s really relevant to the millions of programmers in the world. You can’t really do anything with the computer without a compiler and so I think PL is an opportunity to have a lot of impact by focusing on that layer of the stack instead of single vertical applications.

Soham: Rachit..

[01:08:46]
Rachit: Cool. I’ll start with the pitch for PL and explain why it makes sense. I think when people look at problems, they often think there are parts of the model they are working with fundamentally immutable. I think a lot of people…

[01:09:06]
Soham: Fundamentally immutable you said?

[01:09:08] Rachit: Immutable, meaning you can’t change, or can’t replace say an x86 processor out of a machine. You can’t make that assumption for some set of problems. I think a lot of people have solved problems assuming the language is static, assuming the language can never change. This is a thread that could run through research like we were talking about before where HLS is solved by compiling C or C++ down to hardware because people fundamentally believe that languages are immutable.

[01:09:34]
Soham: HLS is high-level synthesis, is what you’re talking about..

[01:09:37]
Rachit: Yes. HLS is high-level synthesis. I think just the thought that you can change a language to solve your problem is really powerful. If you do that and try to solve problems through this perspective where changing the language is totally fine, is a really good way of approaching PL research, systems problems and even theory problems.

My biased answer of what should people work on, what should people care about is programming languages for hardware. I think there’s a remarkably few number of people who have thought of hardware design as a compilers and languages problem, and there’s a very good discussion. I’ve been recently addicted to reading this thesis from the 1980s. It’s called ‘A Bulldog Compiler’. I recommend everyone who works on compilers or hardware should read it…

[01:10:29]
Soham: Whose thesis is it?

[01:10:31]
Rachit: This is a thesis by John R. Ellis from Yale University and the thesis came out in 1985. It’s a really good discussion of how compiler design affects hardware design and how hardware design affects compilers research. There’s a really good discussion of, Sometimes hardware people think something is really good or an efficient primitive, but they totally ignore the idea that a compiler has to compile down to it. Once you think about it from the compilers perspective it’s totally impossible to use the same abstraction you’re building. So that intersection of research remains relatively unexplored. There’s a lot of opportunity for a lot of really cool work in the intersection of compilers, hardware, and programming languages research.

Ed note: John R. Ellis’ 1985 Yale PhD thesis – Bulldog: A Compiler for VLIW Architectures.

[01:11:16]
Soham: Adrian.

[01:11:17]
Adrian: So here’s a wacky idea I think people should maybe work on. There’s a lot of things in computing that are bordering on being programming languages, that a lot more people use than ordinary programming languages.

[01:11:34]
Soham: Like Excel?

[01:11:35]
Adrian: Excel is a great example. I even think the block-based learning programming environments like Scratch, that we teach to kids are another example of this. It’s kind of Programming-y, but it has it’s fundamental trade-offs with respect to what you may call a real programming language. Something that someone should work on is taking stuff like Excel and Scratch, and other ways that thing approach programming languages. Did you ever make a smart playlist in iTunes? There’s a series of rules you can craft in order to select the music that you want to show up in it.

[01:12:15]
Soham: It should be mentioned that Adrian works on an open source music organizer.

[laughter]

[01:12:20]
Adrian: Those things. It’s like you’re building up what look like logical formulas with a bunch of radio buttons and dropdown menus, and obviously they’re way more accessible than if you had people write Python in a little box to choose what you want to select into your playlist. I think gathering up all that stuff, all these pseudo-programming interfaces, and figuring out ways to gradually let them turn into proper programming when you want to, without sacrificing the user-involved interface that you still have, could be someone’s higher calling. It’s a way to expose the power of proper programming languages in a context that lets people gradually step into it as opposed to the need to flip a switch from just radio buttons to just Python. Some sort of gradual series of stepping stones that take you into that power-off.

[01:13:16]
Soham: So, you’re on a spreadsheet and you’re doing some more things, and then three months later you’re like ‘ah, I’m doing it, I’m actually writing a program’.

[01:13:24]
Adrian: Totally. Yeah. At some point when you’re making a great spreadsheet. I think everyone who’s made an interesting spreadsheet wishes there was a computer in it (it was a computer nerd, obviously)…

[laughter]

Adrian: .. where you could write a function with arguments and return… And if there was a way to gradually step into that without flipping entirely away from Excel which has its own set of advantages, then we could not only make things less frustrating for nerds but make things more powerful for millions.

[01:13:51]
Soham: And this would tie in a lot of threads right? Because you would not be able to do this sort of theoretical work of figuring out how such a gradated language would work. You need to do some usability stuff to figure out how you anticipate when someone’s going to need something, because you want to give it to them when they need it. When they go ‘ah, I need this function thing!’ and then they go ‘Ah, it’s offering it to me!’

[01:14:08]
Adrian: Yeah. Here’s one little piece of programming that you can introduce to your programming life.

Soham: It’s like, Clippy, but better. That could work!

[laughter]

Adrian: A PL person’s Clippy, right!

[01:14:18]
Soham: PL Clippy! Steal this idea, apparently, Adrian’s not working on it, so you could! Actually I like this a lot! Okay, 30 second pitch.

[01:14:26]
Adrian: Thirty second pitch for caring about programming languages – it’s just about the attitude thing. So rather than the individual problems that we solve, there’s something about programming languages – it’s a lens of looking at problems that is uncompromisingly precise. We’re all just huge nitpickers – we really want to actually understand how things work instead of getting just a rough notion of how things might go. That kind of attitude that you implicitly learn by taking programming languages classes can be super useful across lots of domains.

Soham: Okay, so an argument for nitpicking.

Adrian: Mmhm!

[01:15:04]
Soham: Alright! Thank you! This has been very enlightening.

Adrian: Thanks, this was fun.

Alexa: Thank you!

Rachit: Thank you!

[disconnect tone]

[01:15:11]
Soham: Thanks for listening to that episode of Segfault. You can find Alexa VanHattum on Twitter at @avanhatt with two Ts. Rachit Nigam at @notypes, Adrian Samson at @samps. You can find yours truly at @sohamsankaran, and at my website soh.am. If you liked this episode, listen to some more and subscribe at honestyisbest.com/segfault or via your favourite podcast app. We’d appreciate it if you shared this episode online, and in particular, with anybody that you think could benefit from it. Segfault is a production of Honesty is Best. Find more of our work at honestyisbest.com. [01:15:50]