Hello, and welcome to the Future of Coding. Today I have James Koppel on the podcast. James is a Carnegie Mellon grad. He's also a Thiel Fellow. As part of his fellowship, he started Tarski Technologies, where they did program repair, which we're gonna hear about in a second. He's also worked at Semantic Designs, also in this field of tools for programming languages, which we'll hear about soon. He's currently doing a PhD in programming tools at MIT, and runs a coaching business helping programmers become better, more advanced. So, welcome, James.

Hello, Steve. Glad to be here.

Yeah, really excited to have you here. I think there's a lot of really interesting topics that you are an expert in that, kind of surprisingly to me, I don't know very much about, so I assume many of our listeners might also know not very much about. What I'm trying to say is, there are a lot of topics in this field that are a kind of trodden ground. You're familiar with topics that aren't part of that.

Yep. Yes. I always like to joke about some of the fads, like deep learning. No one likes it because it's too popular, and it's definitely me. I'm contrarian at heart. I like things because they're obscure, because I think they're important, but underappreciated. I'll be happy to share a lot of that today.

Reading some of your writings, I got the sense that you are someone who has been in this field for a little while, and you've gone down a lot of paths that proved to be dead ends and then backtracked and then gone down different paths. I thought it was interesting to follow your story in that kind of more narrative way so we can try and learn some of the lessons you learned the hard way, but a little bit easier, because we just can listen to it as opposed to living it like you did.

So I thought we'd start at the beginning. Who or what were your first influences that made you excited about working on improving programming at the tooling level or at the language level?

So probably the best thing that had ever happened me is, I don't know what it was, just some combination of having seen the words, "This project will be rewritten," one too many times. One day in May 2010 I just woke up and it hit me that the world does not know how to write good software. Ever since then, I've been very passionate about programming tools, and I happened to be in a very good place to suddenly get that passion.

Carnegie Mellon is the world's number one university in programming languages and software engineering. It's one of the relatively few top schools to have a very strong research group in software engineering. So, a huge influence in my early development was Jonathan Aldrich, who was my undergraduate research advisor at CMU.

What kind of work did you guys do together, and what kind of work is he known for?

Funny enough, he is one of the very few people in programming languages research who actually designs programming languages. He has a pretty famous feud with another top type theorist, Bob Harper, about whether it makes a difference to a language ... Bob Harper would say that SML and Haskell both have monads, there's no difference. Jonathan Aldrich says it's actually very important to the language design that monads is in the Haskell standard library and there's special support for it, but not in languages like OCaml or SML.

The big thing that we worked on together was the Plaid language, or typestate-oriented programming. Typestates become a little bit more well known in recent years because of Rust. Things like the borrow checker in Rust are forms of typestate.

Typestate's all about the idea of ... Types let you prevent a program from passing in bad values, so basic things like you want a string, you can't pass an integer. Also more advanced things like you need a positive integer or you need a valid person. Typestate lets you put protocols in the type system.

They found in an empirical study, I think the number was that 13% of objects have some kind of protocol. That means that methods must be called in a certain order. So they can, for example, say for files, you must open them before they're read. In Plaid, you'll actually have separate types of file for open file and not, and a closed file does not have a read method. But when you open a file, it suddenly transitions into an open file.

He got a lot of press a few years ago for the Wyvern language. Its big thing is TSLs. You've heard of DSLs, domain-specific languages. These are TSLs, type-specific languages. The idea is that I have a function, which takes in a regular expression or some HTML, so its type is, say, regular ... it takes in a regular expression. Well, if the compiler sees that and now it switches to a regular expression parser or an HTML parser, and so you can mix many different languages, many different syntaxes into the same file in a way which is a lot more principled and elegant than other solutions. It was funded by the NSA, because the NSA does random security things, which, somehow that part of the headline got a lot of news.

The monad feud, that sounds fascinating, but I didn't quite catch the disagreement there.

At CMU especially, there are some very hardcore theoretical guys who believe that the core semantics of a language are all the matters, the core type system. So if I add a feature to a programming language but that feature is very difficult to use, they would say that programming language has that feature, and that's what matters. And Jonathan actually thinks it's important what people actually do with the language.

Got it. Okay. And then these TSLs, I didn't quite catch the difference between them and DSLs.

It basically is a DSL, but ... So, you call a function. This function expects an argument of a certain type. Based on that type you can just declare a parameter with a DSL, and the compiler knows which DSL to use based on the type.

Oh, okay. I got it. That makes more sense. Okay, I got it. That makes a little bit more sense to me. Okay. Cool.

There was a quote that you had sent me that the claim was that software maintenance is the number one solvable impediment to social progress.

Yes.

Did you believe that early on, or was that something that you came to realize over time?

I don't know exactly when I started to believe that. Back that up a bit. Obviously, saying the largest is a very hard claim to make because you have to go through every other possible candidate and do a comparative quantifier. I will defend the claim that it is a very, very, very large impediment to societal progress in that all kinds of change are at some point limited by our ability to change software, and this change is far harder than is needed, and there are also are very, purely technical solutions to the problem, technical solutions that can reduce the cost of software maintenance by a factor of 100 in a relatively near-future time frame. So, over the course of a couple decades.

Got it. Okay. That makes a lot of sense. I think I want to harp on the word you use, software maintenance. It seems like a word you use a lot.

Yep.

In my mind, software ... I guess I'm kind of getting at, how broad is maintenance? If you have a program that lives for a long time and you're constantly adding to it, is that ... Because to me, maintenance is more like just making sure that it continues to run. But is incrementally adding features also maintenance?

Yes, it is. Basically anything that someone with the job title Maintenance Programmer would do is maintenance.

So not an application developer. If I'm a regular software engineer at-

Any developer does maintenance, so a lot of the examples I have in mind are ... any policy change.

The Social Security Administration has, I think it's about 60 million lines of COBOL. The joke is that it's one line of COBOL per retiree. Their application talks to 500 separate databases, so any time when you want to pass a law that changes Social Security, you throw that over the wall to the SSA and people there are going to have to modify this 60-million-line COBOL program. That's just one government agency of many.

I know their story there because Semantic Designs did some work for them on doing program comprehension tools. Basically any change you want to make to our institutions, if that institution runs on software, as does the SSA, then you have potentially a very, very large software maintenance problem. That makes the change much harder to roll out.

Yeah. That makes sense. I think, when I hear "maintenance," I think of a much more narrow definition of maintaining the status quo as opposed to the more dynamic definition you're talking about.

But anyways, I agree with you, and I feel like it's not talked about enough. I think people focus more on beginning new projects, which to me is crazy because that happens once, and software maintenance is every other kind of programming, and it's the most important kind. So anyways, I'm with you.

It was a fairly recent development where I realized, oh, wait a second, it's big projects, tens of thousands or hundreds of thousands of lines of code, are the ones that we should be thinking about.

Yep. They don't get all the flashy announcements, but that's where most of the labor is spent.

Yeah. Okay, so continuing chronologically, it sounds like your first real adventure post-university was with your company, Tarski?

Yeah.

And you guys did program repair? So maybe talk a bit about what that is and what you tried to do.

Sure. Program repair is exactly what it sounds like. It's a problem of automatically fixing bugs in other programs. The general way that this looks is, you start with your original program, which has a bug. The bug is exhibited by some failing test case. You perform some kind of search for a modification to that program in order to make the test pass.

The genesis to this was really, when I started the Thiel Fellowship, I was looking for things to do, preferably things which would let me keep working in this area once the Thiel Fellowship money ran out.

I was giving a talk at the Singularity Summit, basically trying to argue that advanced tools that can accelerate the pace of programming are possible and coming/here. I came across the program repair work, and in late 2012 this was starting to become a hot topic because in ICSE that year ... ICSE is the International Conference on Software Engineering. It's the largest academic software engineering research conference. Claire Le Goues at University of Virginia, she's now a professor at Carnegie Mellon, and her co-authors, they published a paper called "A Systematic Study of Program Repair: Fixing 55 out of 108 Bugs For $8 Each." I found this paper as I was doing research for my talk, and I was pretty blown away by the results. This sounded like something that could be pretty immediately commercialized. So I started working on this probably a little bit or a lot too fast.

Basically, I didn't know all the things that you have to check to make sure a startup idea is a good idea. People talk about, oh the idea doesn't matter, it's the execution. That is totally false, because ... Oh, ideas are a dime a dozen. And product ideas are a dime a dozen, but ideas with the potential to germinate into a business with a sales plan, with a marketing plan, with a growth plan which are defensible, things that can be done now, things where you can create a crappy prototype and still sell it and not have to have the thing perfect in order to work, those ideas are very rare. I did not know the kind of rigorous testing of the idea that needed to be done before committing to it.

There are also some specific issues to trying to build a company based off research, especially research which is not your own, which is, first, understanding that academics usually are a little bit pompous. Part of their job is to craft a really nice story and a presentation to funding agencies about how their work is going to have a huge impact. Often the story is based on ... it's a little bit idealized. There's a particular controversy with the GenProg program repair work I was working on, which I can talk about in a minute.

There's also the fact, you can never turn a paper into a company. You turn a research area into a company, but not a paper. And even if you read and understand every paper in an area, that does not make you an expert in the area and it does not mean that you will be able to instantly respond to different variations with your problem or modify the work to overcome barriers, know what issues can come up. So much of that stuff is hidden, and there's not really a good way to get it other than hands-on experience.

I was basically in the position of learning three very hard things the hard way all at once, which is business fundamentals; general software engineering stuff like how to build a distributed cloud of different program repair servers, because this was a very computationally expensive approach, you're running hundreds of thousands of variants of an industrial program; as well as learning the research side. That was a bit too much at once.

I believe it. You said you were going to talk a bit more about the GenProg approach?

Oh, yeah. Program repair has become a pretty hot topic nowadays. There are dozens of papers published in conferences every year about it, probably on the order of 10 or 20 research groups working on this. There is now an entire website, program-repair.org, which collects all these. I actually used to own that domain, because I bought it during my Tarski days, but I sold it to someone who manages it now. So the field has advanced a lot.

But I was kind of doing this in the early days. At this time, GenProg was the only game in town. The way it works is almost too simple, which is, they have a pretty restricted space of patches. So they're trying to create a patch script. A patch script has sequences of three kinds of commands, which are copy one line of code from one place to another; to delete a line of code; and ... let's see, where are they ... I think it's insert, replace, and delete. Some variation of that. It's been a while.

It doesn't invent new lines of code from scratch?

Yeah. Yes. It only copies things from one place in the program to another, because in their particular approach, they did not have ... If they were to try to invent new lines of code, they did not have a very good way to prune the search space, so it would be way too hard.

Yeah. I got you.

So, something that I discovered, which ... As a side note, which has actually become pretty important to the research I do now, program transformations tend not to work on the original source code. They usually preprocess it into a simplified version first. Because of that, it's actually is very hard to render the changes back to the source tree. So for the original system, it was actually pretty hard to understand what it was doing, because you'd get a result on preprocessed code. It's not obvious ... It inserted a line in this preprocessed code. That line corresponds to part of a line of the original code, and it can be hard to understand what exactly happened. So even though I had all the results and I saw all the changes that it made, it took me quite a while to realize that the patches it was producing were actually quite bad.

A later researcher, it was actually someone at MIT, discovered that the main way it worked, most of its patches actually had the effect of just deleting code until a test passed, which is still potentially useful. I sometimes do debugging just by commenting out half my code, commenting out half of that. But much less useful, especially for something that's this sophisticated and this expensive, computationally.

Got it. That makes a lot of sense.

By the time I discovered that, I already was quite invested. Basically I was stuck. It's like, okay, I need to do a different kind of repair algorithm, and there weren't very many published at the time for me to draw from.

So at the very end of the days I tried switching to a different algorithm based on a paper called PAR, which used a small number of patch templates. Of course that work had its own problems, which is that it was later pointed out by another guy, Martin Monperrus, now in Sweden, that most of that system ... Their system reported, oh, it could do all these patches, but actually mostly it just fixed null pointer errors. But that was also not obvious from reading their paper. It's a reason, especially in programming languages where every paper is reporting on a 10,000-line system, reading the paper does not give you a very strong understanding of what actually happens.

Yeah, that does seem like quite a problem. Now I could see more what you mean, that it's hard to implement someone else's paper in a company setting.

Yeah. Basically, you should be an expert in the field beforehand, or you should be in an R&D department where you have time and funding to become an expert first.

That makes sense. I'm trying to think ... I actually ... of examples that violate this idea. Or I'm trying to think of companies that came from academia, and-

I'll give you one that might not be on your radar. You've heard of Agitar Software?

Addepar?

Agitar. They have an-

How do you-

A-G-I-T-A-R.

No, I haven't.

Agitar was a bit of a big name in the early 2000s. It was founded by a couple people who had previously founded another successful company. I think it started with a V, but ... They already had done a major exit. Two of the founders were Roongko Doong and Alberto Savoia. I've talked to both of them. They might have had a third co-founder. I believe Roongko does have a PhD, or at least one of them does.

Their idea was based on a very famous work by Michael Ernst, who's now at the University of Washington, called the Daikon. Daikon is dynamic generation of program invariants. It's an idea which kind of sounds simple, and I've heard random people suggesting similar, but it still was surprising that it worked this well. Enough that Michael Ernst's advisor told him that it was never going to work, and then 10 years later he won the best, most impactful 10-year paper award for it.

Wow.

The idea is basically, if this function runs a lot, and every single time it's run x is greater than zero, maybe x > 0 is an invariant. You can then present this to a user and say, "Is x > 0 an invariant of this function?" They say, "Yes." Cool. Now you have that. You can use it in verification. You can also generate tests from it. So it would generate a test that x is greater than zero.

That's essentially what the Agitar Agitator did. It would do various kinds of random fuzz testing on your program, it would present you a list of invariants, and it would generate tests from it.

That's cool. And it worked?

Yeah. My impression is that they basically had been just directly inspired by that paper without other ... and maybe it was a lot of general technical experience, but not exact expertise.

I'm also told that there were two other companies that people tried to found based on this Daikon idea, but the other two were much less successful.

Agitar was in the tens of millions. I think they hit about 25 million in annual revenue, and then the CEO said, we have 25 million revenue, the market's too small, and they shut down the company. That's another interesting story.

That's kind of wacky. I guess maybe their revenue wasn't sustainable?

When I talked to Roongko, the summary he gave was ... He just said getting there was very hard. Some things happened. One thing is that, when they started the company, I think they started in the '90s, or at least around 2000, it was pretty common that companies would pay thousands of dollars for an IDE seat. Then IBM open-sourced Eclipse, and the tools market in general cratered a bit. Today we have the culture that people are always chasing freemium models or trying to indirectly make money off tools, because there's now a culture of everyone expects tools to be free.

This is another of my big beliefs right now, that we're in a feedback loop where people don't want to pay for software tools because software tools worth paying for aren't really out there, and people aren't making software tools worth paying for because no one's paying for them.

An initiative I've been toying with for a while is trying to convince a bunch of open-source tool developers to refuse to give away their stuff for free, in hopes of breaking this feedback cycle and getting a more functioning tools industry. But that's something I'm not sure will work.

Yeah, that's tricky. I guess a lot of us have been thinking about this question of sustainability in open source. Have you seen Nadia Eghbal's work?

Nadia who?

I don't know how to pronounce her last name. I think it begins with an E. I think on some places she goes by "nayafia." She has a lot of work on the sustainability of open source and creative models to fund things.

Okay. I'll check that out.

But anyways, what I was going to say to your plan is, I agree with you. It's a hard sell. Price is a function of supply and demand, and the problem with software tools, from my eyes, is that the supply is so high, like it's infinite, that the price will always be zero.

Yeah.

It's similar to how everyone wants to be an actor.

Well, so, the supply of individual, already developed software tools is infinite, but the price ... For most software tools that we can build that would be very valuable, the supply is zero. This is one of the big driving ideas behind the business model of Semantic Designs, which is, they spent 20 years building their DMS infrastructure, making these tools easier to build.

What does DMS stand for?

DMS stands for Design Maintenance Systems. Basically think of a standard tool that you'd use to build the compiler, like the parser generator, pretty-printer generator, static analysis frameworks, all that stuff, and just think that some crazy guys in Texas spent 20 years building this very fancy, very integrated infrastructure that no one else understands.

They can do some pretty crazy stuff in a short period of time, but it has only been a couple occasions when they've been able to sell the same tool twice. Usually someone comes and says, "I have IBM COBOL 8. I want you to translate it to Java." And they say, "Cool. We built a tool for that for another company." Then they discover it's a different IBM COBOL 8, and they have to build a new tool just for them. And they say, "Sure, we can do it. The price is a million dollars." Usually people walk away at that point. So most tools that would be really amazing are just not going to get built, so supply is zero.

That's interesting. It's interesting because the demand is so high and nobody's stepping up to solve it for companies.

Yeah, but that's basically the major motivator of my current research, which is, the market is so heterogeneous that amazing things for every problem and every language can be built, and none of them are worth building. So my research nowadays is all about how to make programming tools more general and easier to build.

Got it. Okay. That helps me contextualize your current research. But before we go into your current research, do you want to linger a bit on Semantic Designs and share a few more stories or lessons learned from working with them?

Sure.

They sound fascinating.

Yeah. Semantic Designs is just completely awesome, and not many people know about them.

How'd you find out?

I actually found them a bit randomly in 2012. I googled the word "reengineering," and they were one of the first results. I followed them for a while, and I had a three-hour lunch with Ira in 2014 when I was visiting University of Texas for grad school. He invited me to come work for them, and so I spent the summer of 2016 working with them. Basically I spent those three months trying to download Ira Baxter's brain, because he's been building programming companies since about 1970. He's been doing programming tools for over 20 years, actually really back to grad school over 30 years ago.

Wow.

He has a huge number of war stories that I've tried to download into my brain.

Yeah. So where do we start? What can you share that you think would be interesting to ... Or maybe one way to filter out the stories that you should share is, what has informed your own direction the most? What things did you learn from him that you were like, oh, I thought this was a good idea before, but now Ira has explained to me that it's a bad idea?

A big thing is his stories in implementing front ends for different programming languages. Semantic Designs has over a hundred language front ends. A language front end, it's not just like a GUI. A language front end refers to the parser, the pretty-printer, basically anything that deals with the raw input of a programming language, which is usually the source text, and converts it into artifacts that the other compiler infrastructure can deal with.

So actually, here is my own story from my time there. I got the idea going in that Lua was the simplest real programming language, so as I was learning their stuff I decided to build a front end for Lua for them. And that actually ... that is not the case at all. Lua's super dynamic, and its lexer is non-regular. I think it might even be non-context-free in that just determining where a comment starts and ends requires the ability to match the number of consecutive equal signs in their syntax.

He told me a lot of other stories about other languages which are crazy. So just the problem of decoding input streams is actually kind of tricky.

In Python, one of the first two lines must declare the character encoding of the file, so somehow you have to guess the character encoding long enough to read a string that tells you the character encoding in order to read the rest of the file. They did a project with a Japanese multinational company, and part of the reason they got the job was that they dealt with the Japanese character encoding, which is called Shift JIS. The people were just so impressed they dealt with Shift JIS. That's part of why they got the job.

I think there was some case in Ruby where their lexer ... The lexer is the thing that turns the raw source text into a stream of tokens. So it goes from, like, "Here's an 'i,' here's 'f,'" to "Here's an 'if' token." They have different lexer modes, which is a pretty good idea that other lex generators I've seen do not have, where it could see a character and say, "All right, we're switching to a different lexer now." They have a stack of these modes, and they found some cases in Ruby where they actually needed to dispatch on the current lexer stack.

So people talk about lexing being a solved problem, but dealing with all the idiosyncrasies of real languages is absolutely crazy. You have languages where there are things that are keywords in some contexts, but variable names in others. You have some languages where white space ... every language calls itself white-space insensitive, but there are languages which are more white-space insensitive. You can put white space in the middle of a keyword and it's nothing, or having a space in a variable name.

All this makes me want a checklist from I guess you or from Ira, like Ira's list for things to not include in a programming language to make it ... because it feels like ... or maybe it's easier than that. How can programming language designers not make these mistakes? How can they make a syntax that's easy to parse?

That's a pretty good question, in that there are a lot of these things which to anyone in program analysis would be super obvious that it makes things difficult.

One example is, in the IEC 61131 standard, which is this international standard for certain kinds of control systems, there's one part of it, I think it's the ladder logic language, but there are five different languages in the standard, so don't quote me on which one it is, it's one part of it which is basically a long change of if conditions and actions. If this controller has the signal greater than 80, then do this. Very long chain of this. That could be parallelized. You can try all these conditions at once. Then someone decided to add goto to this language. If you have a goto, then all of a sudden there are dependencies in the control flow between things that used to be control independent, and therefore they cannot be parallelized. They must have some kind of sequential order.

Got it. So to me it sounds like we're talking on two different levels. The goto is on the program verification, semantic level?

All these things kind of fit together as far as decisions you can make in the language design which make it harder to analyze, harder to parse, harder to lex.

I think harder to analyze is on a higher level than parsing and lexing.

Okay, so just talking about lexing and parsing, there's an easy thing that if your own parser and lexer in your compiler infrastructure is easy to write, then so will others. If you restrict yourself to something that could be parsed using ANTLR or using some kind of CFG generator, then other people can do so, too. If you don't rely on parse actions, so if you can parse your program and then interpret it, and not have something that runs in the middle and says, "If you see this symbol, do this," and that affects whether something later is valid, so you don't add any context-sensitive kind of stuff, then it'll be easier to deal with.

Got it. Okay. That makes a lot of sense. I feel like if you ... almost the answer is as simple as, make sure it's a context-free grammar.

Yes.

And does that get you 80% of the way there?

Yeah.

Got it. But I do ... I haven't really thought about that problem too much. My thoughts tend to linger more on where you were going with, how do you make programming languages that don't have bad constructs that decrease your power of casual inference?

Yeah.

And so goto is the classic example, goto considered harmful. But I was kind of going through a lot of the things in programming languages recently, in my mind, and it occurs to me that almost everything is harmful. Or there may be more things to get rid of than things to remain.

It depends what your goal is. There is a very classic tension between flexibility and the ability to reason, in that the more things that could happen in one place, then, well, the more things you can do, the more things you have to think about.

An example of this is inheritance. Inheritance says I can have one function which can be overwritten to mean many different things, and there's dynamic dispatch that determines which one. That lets you do a lot of things, and people have done some pretty hardcore stuff with this. For example, you can take a language like Ruby or JavaScript or Julia. You can override all the basic functions like plus and times in order to return a parse tree instead of actually doing the operation. And you can implement all kinds of advanced tools based on that idea, like symbolic execution. But that also means when you see "x + 1" you don't actually have any idea what's happening. So there's this very beautiful line from a classic essay by William Cook called "On Understanding Data Abstraction, Revisited," which I think is one of the best readings in computer science I've ever seen.

Wow. I haven't heard of this one. Can you repeat it one more time? "On Understanding-"

"On Understanding Data Abstraction, Revisited" by William Cook, who's a professor at UT Austin.

Cool. I'm excited about this.

Yeah. There's also the followup, which, written by my advisor at CMU, Jonathan Aldrich, which I have a teeny acknowledgement on, which is called "The Power of Interoperability: Why Objects Are Inevitable."

Both these are very good, because there's ... Most industrial programmers, and most academic research as well, have a major misunderstanding of what objects and object-oriented programming actually are. Theorists have come up with very good answers to this question which explain them very well, explain when objects are the right thing to use, when they're not, when inheritance is a good idea, when it's not, but most people don't know this stuff.

The reason I brought this up was a little side comment in the first essay I mentioned, which is, objects have been written, designed, to be as flexible as possible. It's almost as if they were designed to be as difficult to verify as possible.

Yeah, I'm with you and I think we all feel that tension. You can describe it in a lot of different ways, like people who like interpreted languages, dynamic languages, versus people who like static languages, compiled languages. It's like, yeah, you have Ruby and JavaScript and Python on one side and Haskell and Rust on the other side-

Yeah. And I want to point out that the generalized version of this tension happens not just in language design but really every single time you call a function, in that the caller has a desire for the preconditions of this function to be as broad as possible so that it can apply to the current situation, whereas the function has a desire to make the preconditions as narrow as possible so the function is easy to write.

That's interesting, because I think when I'm using a function, when I'm the caller, as a programmer, I want the function to ... I'm so nervous, I have no idea what it's going to do. I kind of want it to be as narrow as possible.

So, if the precondition is so narrow that it does not include the current state, that ... so you call it ... that you call it without satisfying the preconditions, and its contract says anything can happen. So you want it to be easy to satisfy the preconditions.

Otherwise I can't even use the function?

Yeah. But if the preconditions are too broad, then it becomes very difficult to change the function because it's used in so many different ways.

Interesting. I think I kind of ... Maybe I'm very much on the ... Reasonability is important to me more than the flexibility, so I feel like it runs in the opposite direction for me. When I'm writing a function, sometimes I'll get tricked into making it more generalizable than it needs to be, but when I'm using a function I really, desperately want it to be as dumb simple as possible so I can understand what it's doing.

Yeah.

I'd rather just write my own function than use someone else's function that I don't understand.

I think those aren't necessarily in tension. I'm also not entirely sure I understand your position right now.

Okay. Well, we can move on. Well, actually, I want to linger on this divide a little bit more, because I think it is fascinating, because it's a little bit dispiriting, I think, for both sides, to think that there isn't a right answer. It's just kind of dependent on your situation?

Well, any time when two components in software interact, it's a negotiation. There is kind of something fundamental about those sides' negotiation wanting different things.

From the perspective of large software projects that we need to maintain, to me it seems like in that context, which is most contexts, large software programs we need to maintain, it seems like reasonability-

So, explain what you mean by reasonability.

... and strictness is so much more important than flexibility, because flexibility is makes it easier for you to write things, but makes it so much harder for you to read things. So for me it's pretty clear.

Okay. This audio cut out briefly. What makes it easier to write things and harder to read things?

Having more flexibility--on any line of code anything can happen--that makes it easier to write things, but it makes it so much harder to read code, even that you've written but especially that other people have written.

Okay. So ...

So I imagine for you, who, you're interested in the maintainability of large programs. You would be much more on the verifiability-

I'm generally a fan of having pretty restricted interfaces. A line I like to repeat a lot is that "the power of a software design is not what it can do, but in what it can't do." Your goal as a software designer is to design it in a way where all the things that you need to happen can happen, and all the things that you don't want to happen can't happen.

Internally, when a function accepts a broader space of inputs, then that goal becomes harder. There's a bit of a ratchet effect that, you have a function with 10,000 callers and that call it in 20 different ways, you must continue supporting all those 20 different ways of calling it unless you go through and change those 10,000 calls. Obviously there's a continuum of this ratchet effect from a function which is called once in the same file, all the way up to the HTTP standard where someone misspelled the word "referrer" back in the '80s and that's never, ever going to be changed.

Yep. I'm with you. Okay.

There's one other question that's semi-related to this sort of stuff that I wanted to ask. Then we can move on to Cubix. This is very specific to me, but I think it might be common to other people, too, so I thought you might have some thoughts here.

I was given a job where I was given a few thousand lines of JavaScript that were written years ago and were written by someone who was new to programming, and so they're unmaintainable. Callback hell, et cetera. So they wanted the code to do exactly what it does now, but just be cleaner, and I just had to do it with my eyes, basically. I added tests, but it just drove me a little bit crazy that I didn't have formal tools to prove that this line of code never happened. It's more complicated than they're after a return statement. There's some reasoning that has to be done in order to prove that they don't happen. It's very straightforward proofs, but I have to do that in my head with no formal tools for these kind of things. I was wondering if you had thoughts on-

Yeah, and that's ... Going back to what I said earlier about most tools that can be built, just the supply is zero. All these tool things that we know how to build that could help you with that, there aren't very many that are actually around.

When I was at Semantic Designs, they have an employee who used to have another company called Black Box IT, and they built some program comprehension tools for COBOL. One of the things they did was this thing called program slicing. Program slicing is an idea invented by Dr. Weiser, or Dr. Weise, in the '80s where you take a program, you pick one variable or one output and say, "Give me just the parts of this program that effect that one output," and it will trace back and find that for you.

I was surprised to find that, in the COBOL world, there actually are a bunch of tools that do this, whereas in the rest of the industry I had never heard of anything actually used commercially that does this. There are lots of academic tools. It's a very old idea, very well known. Nothing that anyone could just download and use.

I'm actually reminded of a JavaScript task that I had to do during my time at Apptimize, which also involved refactoring some thousand lines of unmaintainable JavaScript. The tool that I wish I had at the time is actually a Semantic Designs tool, one of their few off-the-shelf tools, not these custom migrate-your-entire-things but a much smaller thing where they have one of the world's best clone detectors, meaning that it can search through a codebase and discover common patterns in the code. There are a couple of other tools that do this. There's a company called Pattern Insight, I think was acquired by VMware, which can also do this at a much greater scale, so for millions of lines of code, but it's not as flexible in their pattern matching. I looked at the outputs of the Semantic Design clone detector, and I find some very interesting things. For discovering common concepts that it could refactor, it would have been invaluable.

Got it. Okay. You remind me of one other topic I want to touch on before we move on to Cubix.

So there's this whole field, I guess, of program comprehensibility?

Yeah.

I'm fascinated by this field. One approach is program slicing. And what other approaches are there?

I'm not super familiar with this subfield. I'll tell you a couple things I do know. So there's a work from the '90s by Gail C. Murphy and David Notkin which I like a lot. It's called reflexion models, reflexion with an "x." It's basically about this interactive tool for helping programmers build a map of a codebase in their head.

It starts like this: you look at a codebase and you say, "Okay, I think this part is I/O. I think this part is data management." You just mainly write these ideas down. It's like, "This file is I/O." It says, "Okay." And then based on that it generates a component connectivity graph where it says, "All right, here's everything you said was part of the I/O code," and then it draws lines between them for ... I think basically call graph or data references. And you see, oh, there is this sub-cluster within that which is very highly connected, or this thing I said was I/O but it has all these interactions with the data management part. And then from that you can refine your map. You can break things down to finer components, move things around, and try again.

They had a case study where a guy in Microsoft, he was trying to do this big Excel refactoring project. He saw their talk, tried it at work, and after four weeks he said that he had gotten a deep enough understanding of the Excel codebase that he thinks would have taken him two years without the tool. So this is super cool and exciting.

So they built two different tools that did reflexion models, one for C++, one for Java, and you can get neither of them today. This is my go-to example of ways in which tool development is behind, in some ways, where we were 20 years ago.

Got it. Okay. That makes sense. I guess I just wanted to try one thing out on you, and then we'll continue with your story.

The research that I'm working on now is on ... I think it's in the field of program comprehensibility, but I'm taking a very different approach. My approach is that the languages we have today don't lend themselves well to comprehensibility, so we need to vastly restrict what's allowed to do. For example, no goto statements would be something that I'd want to disallow in the language. So, anyways-

As a little side note, I don't think gotos are ... There are intraprocedural gotos, I don't think they are that important for comprehensibility in that if it doesn't affect the interface of the function, then it's a local problem. It makes that one function harder to understand, but not the system.

Yeah. That's fair. That's fair. Yeah. But it effectively turns that local function into a black box, which is okay-

Potentially.

Which is okay if you're okay with it.

I'll point out that in the systems programming world, it's pretty widely known that goto is the best construct in the C language for error handling. So it's still very much used.

Interesting. Well, I guess my question here is, it seems like you're very much taking this polyglot approach where your thought is that tools are too expensive to build for one language, so if I build approaches that allow tools to be built for any language, then that kind of solves this problem?

Yep.

My inkling or my predilection in this ... my tactic is to build a language that's just better, and then somehow-

Yep. Yeah.

... build a language that lends itself to tooling better. So that's how I decrease the cost of creating tools.

Yeah. I think definitely some people will share that idea. A very extreme example was, there is a language called ParaSail, which was created by Tucker Taft. I last heard about it ... I saw a presentation about it many years ago. It basically was designed to be a very restricted language. I think it might have not even let you do recursion. The idea that it would be so restricted that it'd be very easy to write tools for and very easy to super-optimize and parallelize automatically. So that's the relatively extreme approach.

Got it. Cool. Yeah.

So, yeah. Definitely some languages are easier to build tools for than others. That's one of the reasons you see so much academic work focusing on Java. Java, compared to C++, compared to Python, is pretty tame. You can do a lot of things just with the bytecode, which is pretty well designed.

And obviously there is a lot of old stuff in existence, and it's not going away.

Yeah. Yeah, yeah. That makes a lot of sense. But particularly from your experience at Semantic Designs, you're intimately familiar with massive codebases of dead languages.

Yep.

Or I guess the other way to put it is that programming languages don't die.

Yeah. If you get a pay stub, there is a pretty high chance it was processed by ADP and went through a large, 40-year-old COBOL system. Not COBOL, actually not COBOL, assembly, for a dead language. Probably a lot of other things will go through COBOL systems.

The company I started, we use ADP, so there you go.

Cool, so let's stop talking about it. Let's talk about Cubix. Tell me a bit about how you got the idea and what your novel approach is.

Sure. Yeah. Cubix is my framework for language parametric transformation. The tagline is, "One tool, many languages."

So here's a motivating story for why this is important. When I was at Facebook as an intern in 2010 they had a lot of privacy bugs, and it was things like ... In Facebook you can upload private photos or things only your friends should see. You'd go into someone's photos, say View Photos, it would fetch the photos, it would check which ones you can see and show you those ones. That is error prone, because you need to remember to do the same thing any other place where you could view the photos. One place where they did not do that is in the Report Profile button. So if you went to report someone's profile, you could say this profile was bad because of its photos. It has an illegal photo. It would say, "Okay. Which photo do you want to report?" And there you could see all the photos.

They had a lot of other things like this. Another thing was, for a few hours, there is the button that says, "How does Bob see my profile? What does it look like to him?" For a few hours, you would press that button, you were actually logged in as Bob and could see his private messages.

Wow.

So they needed to do a whole program refactoring in order to fix this. Their idea was to an architectural change. They would create a viewer context object, and instead of having to remember to, every time you display a photo, check whether it should be visible, instead you would move all that to a central location. When you get photos from the database, right there you would rule out all the ones which should not be visible eventually.

So they needed to pass through this viewer context parameter through many, many, many tens of thousands of functions. They took a couple dozen of their best engineers off their other projects. They walked them into a conference room called the Canada Room, so this is the Canada Team, and basically they spent every waking moment for several weeks just adding these parameters to function calls.

So as an intern I had this piece of the code that no one else was working on. I wake up one day and get a merge conflict. Who else worked on this? These people did. They added some parameter passing. So basically, a massive amount of effort adding parameters to functions throughout the codebase.

In 2014, Dropbox had a different problem with a similar solution. Right now I'm logged into Dropbox on my PC. Actually have two accounts on this computer. I have my personal Dropbox, and I have my MIT work Dropbox. They also needed to add an account parameter to many thousands of functions in order to implement this. They obviously had a lot of other things, too, but that was a large part of it. And I'm told that it was the number one project for the year 2014. At the time they had over 100 engineers.

So two companies, massive change, adding parameters to functions. This is the kind of thing you could hire Semantic Designs to build a magic button that does for you. But if both of them had gone to Semantic Designs or hired some other program transformation expert, they would not have gotten economy of scale from having the same problem twice, because Facebook: PHP. Dropbox: Python.

This wouldn't be solved via the multiple front ends that Semantic Design has?

They'd have to build the same thing separately. Maybe they could share some code, but not that much.

Got it.

But with Cubix you could build the same tool for both languages, and in fact we did. In our Cubix paper we built a prototype of a tool that does this, and in the space of less than a week we built this prototype and got it running on C, Java, JavaScript, Lua, and Python, which are the five languages that Cubix currently supports. Not yet PHP.

In one week?

Yeah. The prototype is not that sophisticated, but the big thing is that we are still sharing most of the work between languages, because we can using the Cubix approach.

Got it. Okay. So what's the approach? How'd you do it?

It's called incremental parametric syntax. It basically is a recent existing idea, but with a small addition that makes all the difference. It's an extension of some earlier work on modular syntax, particularly something that's well known in the Haskell community called data types á la carte.

Data types á la carte lets you say, I'm going to define a programming language in terms of different fragments. Here's my control flow fragment that has while loops and if statements. Here's a fragment that has goto's. Here's a fragment that has functions. Here's a fragment that has plus and minus. And you can put these together into a language. And I can define a transformation or an analysis that runs on each of these parts separately, and when I put them together I get the transformation or analysis for the whole language.

Some people took this, made it better, made it easier to scale, but they still have the problem that if you wanted to do this for C, what you would do is you would basically take every piece of C--the C spec is about a hundred pages, which is small for a language spec--and you'd go and implement every single part as a generic fragment. So you'd have a generic function fragment that handles C and hopefully some other languages. You'd have a generic pointer fragment. Everything single thing that's in C, you'd somehow need to model generically. This is very hard because, basically, if you had generic functions which would be used in C and Java, you would somehow need them to be the same, which they're not. So this approach couldn't really handle mismatches between languages. Whereas, say, language parametric transformation, sharing code between tools between languages, it should be possible because languages are similar, but it's hard because languages are also different.

So we made a small addition to this idea called sort injections, where basically I can now say things like, "Here is a generic function declaration, and it has a list of arguments." But what an argument is differs by language, and I have the way of saying, "For this language, this is an argument."

Similarly, for variable declarations I can say, a variable declaration is a list of left-hand sides, is a list of declaration binders. Each declaration binder potentially has some attributes. And then for each language I can say what those things are. So in C, a declaration binder could have a pointer. In Lua, you can declare many variables simultaneously and say "var x,y" or as a list, which you can do in JavaScript, too. In Java, you can have attributes on each declaration, like you can say "int x,[y]" and x is just int, y is an array.

I'm with you. So this makes a lot of sense.

Yeah. Whereas in JavaScript you don't have that. So you have this nice thing where different languages share common parts that you can write against, but you can still capture all the idiosyncrasies of each language.

Cool. This makes a lot of sense. I just want to backtrack a bit. I have two questions.

The first one, so you mentioned this data structures à la carte thing, which sounds fascinating. I, and I imagine a lot of listeners, are pretty familiar with Haskell, so could you explain how this is used in Haskell?

Sure. And it actually is a new name for an even older idea, from the term rewriting community called sum of signatures. I think the best way to understand it is to take a step back from ...

So, Haskell has algebraic data types. You can say, "data tree equals leaf of int or binary node of tree, tree". You can take a step back from that and look at the theory of how these are defined. They actually are defined in three separate phases.

First, each of those things like leaf, node, those are called constructors, and they're just tuples. A leaf has an int, it's a tuple of int, a one-tuple. The interior node is a pair or a triple. Say it has two children, and another int. So that's the first step is getting these constructors.

Then you can say, a tree is one of these many constructors, that's a sum, it's an or. And at this point I've said ... really I've said, these are what my nodes look like, but I don't have the trees yet. So maybe I could say my language has an add node, and it can add two expressions together. What's an expression? I haven't defined that yet.

The point at which you define what the expressions are is when you do a fixpoint. When you add recursion to the data type, you can say, "Feed this thing back into itself."

So when you just have a list of different node types, but you don't know what their children are, this is all very modular. It's only when you add the fixpoint, you tie the recursive knot to say, that it becomes very tied to the current state.

So what data types à la carte does is, it lets you program against signatures rather than term types. So you basically write things in a way of, an add is a plus of two expressions. What is an expression? I'll tell you later. And you leave a type variable for what the children are going to be. And at some point later you say, so I defined this list of nodes, which is either an add or a multiply or an if statement, and they have children. What are those children? Now I'll tell you. It's the thing I just defined. That's the recursive fixpoint.

Okay. I have a little more clarity. So to speak it back to you, it sounds like the sum of squares and this data types à la carte are essential to the implementation of algebraic data types?

In the actual type theory, an algebraic data type is defined from three basic type theory components: recursive types, sums, and products.

Got it. Okay. And a tree with two nodes, that's a sum.

Yeah. So the product is saying, I have a type variable T, T-cross-T, it's a pair of Ts, but the T is a variable. The sum would be saying int plus T-cross-T, so it's either an int or it's two of these T things. I haven't told you what a T is yet. And then the final stage is to say mu of T dot int plus T-cross-T. So there you say what is a T? It's one plus T-cross-T. That's a recursive type. And when we actually spell it out it becomes, what's a tree? Either it's an int or it's two ints or basically ... when you actually substitute one plus T-cross-T in for T recursively you get this infinite sum, which describes every single shape of s binary tree.

Got it. Okay.

It's pretty fascinating. There was a great reading, which unfortunately I ... I can send a link out, because now you have to go to web.archive for it. It's off the internet. But it's called "The Algebra of Algebraic Data Types," by Chris Taylor. It's a multipart series, and it shows you how you can use manipulation on these algebraic data types and find a lot of cool properties.

Is it ... okay, cool. I'll add that to the notes.

Yeah. There's another article, which I think is a lot less good, but it still exists on the internet without web.archive, which is shorter. It's called "The algebra (and calculus!) of algebraic data types."

It sounds like your approach in Cubix, the parametric ... Can you repeat the phrase for me?

Incremental parametric syntax.

The incremental parametric syntax. It sounds to me like that's very similar to this idea of a universal abstract syntax tree. But I know that that's an idea that you aren't so excited about. So what's the difference?

The universal AST is something that I love to hate. The key to the common representation is that I'm going to create a single abstract syntax tree, and instead of having while loops in C and in Java I'm going to have one kind of while loop, and I'm going to translate all of C and Java and JavaScript into this one abstract syntax tree. I'm going to write things in this one thing, and then when I want C or Java back I just output them.

This is how most program analysis tools work. And it works great for program analysis. So architectures like gcc and clang and LLVM, they'll do this. It's like, you'll run gcc on Java or Pascal or Objective-C or Fortran. You'll get the AST for C or Fortran, do some stuff there. It'll change them into, I think the IR is called GIMPLE. It'll change them to some common representation, do some more optimizations, and then from this IR you'll pick a code generator off the shelf and get your x86 or your ARM.

But there are two big things wrong with it. One is that, I've said before, the power of design is not what it can do, but in what it can't do. And it's very important, not just what you can represent, but what you can't represent. So there are a lot of ...

When you're reading a Java program, you have to read it differently from a C or C++ program in that if you have a local variable x, and it's an int, and you call a function with x, in Java, you know that x has the same value afterwards. In C++, that function you call could actually take x as a reference and then modify it, and now you have a different x in the calling function afterwards. So the presence of pointers, and especially references, makes a lot of program analysis things difficult, both computer generated program analysis but also just you reading the code. So the knowledge that your programming language does not have pointers, or not have pointer arithmetic, is very powerful, and just absolutely lost. And that's part of the reason why all these different compiler infrastructures, they will do some optimizations at the language-specific level before going to the IR.

But the other big thing is that when you want ... So, program analysis is easy. You suck everything in. It's okay if you lose information as long as you have enough to still produce useful reports for whatever you're trying to analyze for. But in source transformation, well, if someone types in 0x10 and they get out 16, they're going to be mad, especially the programming transformation didn't touch the part of their code. So you need to keep all this information about language-specific stuff around.

It sounds like that's exactly what you're doing with Cubix.

Yes. Yeah. So in Cubix we don't have a single representation for C and Java or JavaScript. We have a family of representations. Each of them shares common pieces, but each one specific to that language enable it to store or track everything.

So, hold on. To me, it sounds like in Cubix, if I have an assignment in Cubix, that's a data type that is very general that can handle all the quirks of every language.

Yeah, so we have a general assignment data type in Cubix, but it has custom pieces per language.

Got it.

So an assignment is general, but a left-hand side is language specific. But even still, there are some common left-hand sides. So, every language has a left-hand side that can be a single identifier. Some languages have more, but every one has an identifier left-hand side, so I can write a program transformation that can see and identify a left-hand side and do something and know it's something for every single language.

Got it. Okay. To me it sounds like that is a universal AST. It's just not what people thought it would look like.

You can call it that, but the thing is, it's a different kind of type. It's, instead of saying I have a type IR and I'm going to convert all my representations to that and convert it back to different representations, I have a parameterized family, and so I write my types in a different way.

In the talk I gave on this, you can see a recording of this talk on YouTube that I gave to the Boston Haskell group, as well as one I gave in Israel. I have a nice story about how, as soon as you declare the type signatures saying I can convert things to common IR and then back to the different representations, you've already lost. One reason is that when you write down those types, you're basically claiming you can convert any language to any other language, which is too good to be true. So the catch is, you get things like ... There are more than zero frameworks that do use common IR and do try to let you write transformations, and all of them will mutilate the code.

One example is the Compass/ROSE framework from, it's either Lawrence Berkeley or Lawrence Livermore. I think it's Lawrence Livermore. In their manual, they have an example of a program transformation written on C, and it converts all the for loops into while loops, even though it should have been able to leave them the same. Why? Because they use a common IR, and this IR did not have for loops and while loops separately. It just has while loops.

Got it. Yeah. That makes sense.

I have a friend, Aidan Cunniffe, I don't know if you know-

Yep. Yeah. I had a Skype with him the other month.

Cool. I'd be curious to get your thoughts on his approach.

Let's see ...

For anyone who didn't listen to the episode I did with Aidan, he's building a tool just for one language, but it's code generation, so you would explain to his tool how you want to write back-end routes for your Express router, and then it could generate, if on the front end you need some data, it could generate the back-end route for you automatically or vice versa. That sort of thing.

Yeah. So it actually is for multiple languages. They are-

Well, I don't think it's from one language to another.

No. No, it's not. The interesting thing about it, I think, is just identifying the problem, in that he found a problem which is practical but also relatively simple to solve. Simple technology.

So I think that this has a lot of potential. My big point of skepticism is the flexibility of their matching, which is, they're basically using tree patterns, which are a pretty easy thing to come up with, and it is very easy to overestimate, to think ... you think, this is what code for doing this should look like, very easy to underestimate just how much variability you can see in that. Whenever you get into application, what's important is that you find every case where something happens, or even 95% of the cases, then pretty soon you need a much more sophisticated technology.

But I did tell him some of these problems. I told him to look into associative-commutative matching as something which is very important, but will take some architectural changes up front. I found him pretty humble, and hopefully he'll be able to do some great stuff.

Cool. Sounds good. Okay. Cool. Thank you.

Let's talk about the coaching business you run.

Sure.

So yeah, maybe you could give a ... I'd be curious to know how it got started.

So, a fun story. Back when I was in undergrad I was deciding whether I wanted to do software engineering programing languages research with Jonathan Aldrich, or to do cyber security analysis of binaries research with David Brumley. David Brumley has become very famous. You might have heard of the DARPA Cyber Grand Challenge, where basically people program computers to hack into each other and stop each other from hacking into each other. They ran a contest at DEF CON. His team, ForAllSecure, won that contest. So he did some pretty awesome stuff involving binary analysis.

So as I was choosing which professor to work for, at first I chose Brumley. So I was going to take the elevator back to my room to send the email to announce this, and then I changed my mind in the elevator for a very bad reason, which is I thought, oh, maybe if I work for Jonathan Aldrich software engineering research, that will suddenly make me a better software engineer and then I'll be able to do stuff faster. And of course that was silly.

But the funny thing is that over the next many years it actually became true, in that as I got a deeper understanding of software engineering and being able to see the preconditions and postconditions of functions, I actually discovered I'd become very good very fast.

It became very obvious when I joined Apptimize. The person who replaced me at Apptimize, said that my code was like a poem, like one of those beautiful Haskell programs you see, except that this was Java for Android. So that codebase has managed to survive very well, easy to make major ... done some very major architectures to it in relatively short periods of time. Pretty low bug rate. All things that are pretty important, especially given that we were under very heavy constraints to make something with few bugs, because if something goes wrong ... It's an SDK that other developers put in their apps, so if something goes wrong, first, our customers have to upgrade their version in their app, and then their customers have to download the new version. So you want to get things right.

I actually stayed on as a contractor for Apptimize in grad school, so I'm making some extra money on the side. Didn't like living like a grad student. And I had one instance with a coworker where she had committed some bad code, people were criticizing it, she didn't understand what was going on, and I sat down with her and taught her some of these software engineering concepts which are some things that I think some people have intuition for but are pretty non-obvious, and not many can really explain very well. That made a huge difference for her, and just realized how satisfying that was, and also how impactful that was to make her better, because it had much more impact than I can have in an hour just doing it myself.

So about two and a half years ago I started a company doing this professionally. My first client was someone who had just been fired from their job, and a few months later they were a totally transformed person and suddenly were getting offers left and right from Google and Facebook and now are quite senior at the company and having fresh Ivy League grads look up to them. So it's a huge transformation for this person.

So over the years I've crystallized a number of different teachings, which are largely inspired by my knowledge of the academic side. Basically the way I look at it is, every time someone writes some kind of program analysis or synthesis tools, there's some insight behind that about how software works. My goal is to kind of teach this intuition without having someone having to spend years studying type theory.

This is actually a lot of stuff I'm going to talk about in my Strange Loop talk, which is coming up in a couple weeks. One example I really like right now is, if I have a function called sanitize that escapes all single quotes, what you're really doing is that you're creating a notion of a sanitized string which is separate from this function, and this idea of a sanitized string can be hidden, meaning that if I were to write my own code which sanitizes a string exactly the same way, then there's a sense in which it's not legal to use that because the notion of sanitized is opaque.

This is something which you could write down very clearly in a theorem-proving language like Coq, but is something which is almost kind of mystical and ethereal when you just look at normal code, because you're talking about properties and abstract ideas that are not present in the program at all. And in fact so much of what makes good software involves working with ideas that are not present in the code directly at all, something in the design space which gets lost when it's turned into code. And it's kind of interesting that this is an idea which sounds almost kind of crazy and mystical in programming circles, but in other circles it's just mentioned offhand as something obvious.

In a thread that I'm in the other day, the discussion, it's like this famous researcher says you should document the module by saying what secrets it hides, what decisions it's made that can change, no one else can care about, can know about. And the offhand, oh, but this is much harder to extract from the code. It's just not present.

So you mentioned that, how in a language like ... I think it was Coq was the language you mentioned?

Yep.

You can communicate the high-level notion of what you're trying to do?

To some extent. You can write things like, this function must take a sanitized string, this function makes a string sanitized, and set it up in a way where the only way to create a sanitized string is to call that function. And if you write your own function that sanitized that string, then it's not sanitized. You might have replaced all single quotes, but you don't know what sanitized means.

Oh. Well, that I understand. But how about a formal definition for sanitized, to make sure that the definition of sanitized is also-

Yeah, in Coq you would actually write down a formal definition of sanitized. You can make that a private definition, and you can prove that your sanitize function satisfies the definition, but you can't prove that for any function in another module.

Got it. Yeah, yeah. So it's two parts. You describe the ideal, the thing that's ethereal in most programming languages, you can make it explicit in Coq, and then you write the implementation code, the lower-level ... and then you can prove-

Well, in some order, yeah. And-

Got it. Okay. Yeah. You can do it in either order, but they go hand in hand.

Yeah. I see the proof as less important from a design point of view, but just having the idea of some kind of concept which is not present in normal source code, but is present in this design space, is very important.

So is the solution that we should bring it to our code? We should bring that feature from Coq to every language?

Possibly. So, there already is some variation in this. In Python, it is actually very non-straightforward to define an interface in the Java or C# sense, in saying that these are the functions which other people should be allowed to call, here's an abstract description of what they do, which is separate from any specific implementation. You can do that in Python, but you almost have to work around the language to do it, whereas it's just very natural in Java or C#. So a lot of things in that spectrum.

In my business, the angle I focus on is more just teaching people to think like this, even if they are working in Python or Ruby.

Got it. That makes sense. I think that's a great stopgap. Just in the interest of improving programming at the language level, I'd be interested ... Because I think a lot of my best insights for improving programming are taking things that I've taught to students very instructionally, like the way you're doing, and then come up with creative ways to embed them into the language themselves so that they don't even have to be taught because ... embedded.

So with that in mind, I'd be curious to hear your thoughts on almost higher-level languages where you can retain more of the abstractness of your idea. As I've seen you write in other places, when you write an implementation for a high-level idea, you necessarily lose a lot of the notion of what you're trying to accomplish. I feel like you're someone who would know the state of the art on what a higher-level specificationing language would look like. Because I have no experience with those languages.

Yeah, so, I've done a medium amount with a number of different specification languages. I don't have experience using any of them for deployed systems. For that you might want to talk to my acquaintance Hillel Wayne, who is another blogger and expert in TLA+.

Got it. Okay. I think you mentioned somewhere that you are familiar with Sketch, which it sounds like is related to this idea.

Oh, yeah. My lab built Sketch. Sketch is very much not something ... I guess it kind of lets you express your idea at a higher level. Sketch is a general purpose program synthesizer, and its big thing is the idea of a sketch is a program with holes.

Some of the early applications were, you say things like, "Here is a very, very dumb implementation of linked list reversal," which is you just remove stuff and add it to a new list. And then you want the more efficient version of linked list reversal, so you say, okay, I know it's going to involve a while loop, and it's going to involve some combination of these assignment operations. Here's a soup of possible things you can do. Here is a reference implementation. Go find some way to put these together into a program that does the same thing as the reference implementation. And it would.

The way it works, it gets super nitty-gritty in the implementation. It actually does some bit blasting, which means it basically expands your program out to a static graph, unrolls your loops, looks at all the bits that can be in your program, and does solving techniques on the bit level. So on the implementation side it's super nitty-gritty, not very abstract at all. But from another perspective, you can use it to raise the level of abstraction and say, I don't care the details. I just care that it does the same thing as this reference implementation or it satisfies these properties, and here are some constraints on how it works.

Okay. That makes sense. I like to end with an opportunity for you to mention ways, if you're interested in being contacted by people with questions, ways to contact you, places you produce things on the internet, anything you want to get out there or want help with.

Sure. So my blog is pathsensitive.com. I mostly blog about advanced ideas related to software design. You can also check out my papers on Google Scholar or on dblp, the computer science paper database.

My coaching business is jameskoppelcoaching.com. I offer one-on-one coaching as well as a web course and in-person courses to individuals and companies.

The next advanced software design web course is starting on October 11. The course is six weeks. Basically it'll take you through a number of big ideas about software engineering, things that can change the way you view code but are not very well known. You can check my testimonials. I've gotten some pretty amazing results, people saying it made them way better, including both junior people and very senior people. It's done in a pretty structured way, where both you'll do pretty low-level drills with small code examples, and then it'll also give you a walkthrough of a large open source code base and I'll show you how this idea affects this real codebase.

And on something else entirely, one of my side projects for way too long has been the area of binary modification. My other area of expertise, which I haven't talked about at all, is in how to modify programs without the source code and in reverse engineering. Project Ironfist is a game mod for the classic PC game Heroes of Might and Magic II that I've been working on with some international collaborators for a long time. You can check it out at ironfi.st, I-R-O-N-F-I dot S-T, and see how we work our magic.

And of course my personal website, which I'll update some time this year probably, is jameskoppel.com.

Cool. That's awesome. Well, anyways, thanks again for coming on and talking with me. I learned a lot.

Yep. It's good talking to you, Steve.