In this episode, we chat with Dr. Kathleen Fisher, who was chair of the Computer Science department at Tufts University at the time of the interview. We talk about Kathleen’s experience in applying formal methods and PL theory to solve significant practical problems throughout her career. Equally important, we discuss how it came to be that she is practically a pro at golf!
In this episode, we chat with Dr. Kathleen Fisher, who was chair of the Computer Science department at Tufts University at the time of the interview. We talk about Kathleen’s experience in applying formal methods and PL theory to solve significant practical problems throughout her career. Equally important, we discuss how it came to be that she is practically a pro at golf!
Watch all our episodes on the Building Better Systems youtube channel.
Dr. Kathleen Fisher: https://www.darpa.mil/staff/dr-kathleen-fisher
From Dirt to Shovels paper: https://www.cs.princeton.edu/~dpw/papers/learningpopl08-final.pdf
Hancock: https://dl.acm.org/doi/abs/10.1145/331960.331981
PLMW: http://sigplan.org/Conferences/PLMW/ CRAW: https://cra.org/cra-wp/
NSF Broadening Participation in Computing: https://beta.nsf.gov/funding/opportunities/broadening-participation-computing-bpc-0
Joey Dodds: https://galois.com/team/joey-dodds/
Shpat Morina: https://galois.com/team/shpat-morina/
Galois, Inc.: https://galois.com/
Contact us: podcast@galois.com
intro: (00:02):
Designing manufacturing, installing and maintaining the high speed electronic computer, the largest and most complex computers ever built.
Joey (00:22):
Hello, welcome to building better systems, a podcast where we explore tools and approaches that help make us and you better engineers and build better systems. My name's Joey Dodds. I'm a principal researcher that focuses on applying cutting edge techniques from formal methods, uh, to industrial systems that are, that are in live use.
Shpat (00:44):
And my name Shpat Morina. I focus on internal R and D and strategy
Joey (00:49):
Shpat and I worked at Galois, uh, computer science, R and D lab, and we're focused on developing and applying assurance techniques for critical software and hardware
Shpat (00:59):
Today we're, uh, joined by Dr. Kathleen Fisher. Um, Kathleen is chair of the computer science department at Tufts university. And previously she was a program manager at DARPA where she started and ran the hacks and Pamela programs focused on building high assurance systems and software and, um, probabilistic programming for machine learning. She was previously consulting faculty member in the computer science department at Stanford and a principal at, at and T labs research. We're excited to get to speak with Kathleen today because she has a wealth of experience in academia, as well as industry R and D labs in kind of applied assurance methods and what actually works when it comes to making systems better. Kathleen, thank you so much for joining us.
Dr. Kathleen Fisher (01:46):
Thank you. My pleasure. Thanks for having me.
Shpat (01:48):
It is our pleasure to have you. Uh, so the rumor mill says you're a pretty good golfer.
Dr. Kathleen Fisher (01:59):
My dad was a very good golfer and, uh, you know, he played when he was a little kid, he played on the Stanford team when he was in college and he played all his life. So he was in fact, a scratch golfer his entire life, as far as the entire time, I knew him. And when I was about 10, he decided that I was old enough to play golf. And so he started to take me out to the golf course. And, um, I also played baseball when I was a little kid. I played little league and then I played pony league, which is for like seventh and eighth graders. I was the only girl to ever play pony league in my town, at least as far as I know, like maybe afterwards, there were more girls who played, but when I, uh, finished pony league that's eighth grade, it was like time to go to high school.
Dr. Kathleen Fisher (02:38):
And I wasn't good enough to play on the boys' high school baseball team. And like softball was just like, I hated softball. The ball is just like too big and it kind of goes thud instead of THWACK and not very satisfying. So I, I stopped playing. I didn't wanna play girls softball. So I, I started playing, um, golf instead in, in high school. Um, at that point I started playing every day after, uh, school, every day on the weekends, my dad and I would go down to, um, the Palm Springs area in California and play golf on the weekends. We would play 18 holes in the morning and then we'd have breakfast and we'd play 18 holes after breakfast and then we'd have, uh, lunch and then we'd hit golf balls. Um, and I'd do my homework and we play again on Sunday. Um, I, I was captain to the men's golf team, uh, in high school.
Dr. Kathleen Fisher (03:26):
I, I made the Stanford varsity team. And then in college I decided I had time for two outta three of golf of social life and academics. And I decided I didn't wanna be a pro golfer and was much more comfortable making money. You, uh, li earning my living at, as an academic or, you know, with my, I, I don't have the right temperament to be a golf pro. So I made the right decision and I, I dropped off the golf team and I, uh, became an academic instead, but I still quite like to play golf.
Shpat (03:52):
I was gonna say, it sounds like we very easily could have been interviewing a, a pro golfer
Dr. Kathleen Fisher (03:57):
Shpat (04:40):
Oh, I, I bet. Did you say you were a captain of the men's team?
Dr. Kathleen Fisher (04:44):
Yep. Uh, my high school didn't have a women's golf team. And if you don't have a women's sport, then you, the women can play on the men's team. And they made me the captain of the men's golf team, my senior year in high school. That's fantastic. Good training to be a computer scientist
Shpat (04:59):
Oh, I bet
Joey (05:01):
I bet. And all the, all the dedication and hard work is obviously something that is, that is carried into your academic career and you've covered quite, quite a range of topics. And so I guess I, I'm curious, you know, with all that, with all that dedication behind you and, and that hard work, how do, how do you decide what it is you want to work on? What drives your research agenda?
Dr. Kathleen Fisher (05:23):
Yeah, so, uh, my father kind of was relevant in that too, and that his advice in like picking a career or picking a thing to work on was always, um, you know, what matters is what you do on a day to day basis? Like, like what's in, like what's in your inbox. What, what has to go in your outbox? Do you have an inbox, you have an outbox, who do you work with on a regular basis? Um, that kind of generalization of like, what do you, what do you actually do day to day, or moment to moment is kind of like how I've chosen things. It's like, not, it's sort of the opposite of a strategic decision in some sense, or it's like, what you're strategizing for is having a good time. Um, like in some sense, like if you're enjoying something you're much more likely to spend a lot of time doing it and becoming really good at it.
Dr. Kathleen Fisher (06:06):
And if you're really good at it, you're likely if you enjoy it a lot, you're likely to become really good at it. If you're really good at you're likely to do well, and then you're likely to have more choices. And so, so partly that, um, that paired with actually being strategic, I think, is the optimal, um, strategy. Right. Um, I, I, you know, I do think that like, that's how I picked my thesis advisor, cause I liked working on the problem and I liked working with the person. So I, I think I might have been more like, I think programming language theory is not the most strategic area to go in as a PhD student. I think, you know, like no matter what time period, there's something that's more strategic than PL theory. But I really liked like the mathematics of PL theory really appeals to me.
Dr. Kathleen Fisher (06:45):
I just like the, the there's something beautiful to me about discreet math and about models and about symbols and how they all fit together. It just is, um, it's beautiful to me and I like thinking about it and I like to working on it. And so that's how I picked working on that topic. And then I went to At&T labs research when I graduated because the job market was terrible and they offered me a full-time job, which seemed like a really good deal. But after they hired me, they were like, why do we have a PL theory person? We don't really need a PL theory person. Um, so I'm like, Hmm, I better do something that the people who pay me actually think is useful. So I started to work on domain specific languages and that I, I really, really liked because I could, um, talk to customers like people who had real needs and I could figure out how to use the things that I liked, which was designing languages and thinking about languages to solve problems that they cared about.
Dr. Kathleen Fisher (07:38):
And I discovered that I, what I really like is solving problems and I don't really care what the domain is that those problems are in. It could be in PL theory, or it could be in organizing a computer science department, um, or in, you know, hitting a golf shot. Like what I like is figuring out where something, isn't the way it should be, what tools do I have, how, and I make it better and then actually go and make it better and then evaluate like, what went well and what didn't go well, how can I improve that even more the, the next time? And so like that, that my core competency in some sense is really problem solving. Um, and I just like making things better. That's
Shpat (08:14):
Interesting that when you thought about how to make things better at, at, at and T research, it was like, all right, well, let's apply that, that PL theory, uh, into creating, designing and implementing domain specific languages sounds like, sounds like that was something that was actually useful. I wonder if you can expand on that a little bit.
Dr. Kathleen Fisher (08:32):
Yeah, sure. So they had, um, statisticians who were doing this at the time completely out of the box, really crazy thing, which was trying to build profiles of individual customers based on the telephone calls that they were making. So right now that sounds like, well, duh, but at the time that was like impossible. Like nobody could do that because like the whole idea of doing that was brand new and the scale to do that was off like having the memory and the computational cycles necessary to process all of yesterday's calls before the next day's calls came in to build a profile of a customer was super challenging computationally. They were like, they worked super hard and all they could do was keep like two bites per customer. They had to process like 350 million telephone calls for about 350 million customers every day. And the performance limitations were such that they could only do two bites per customer.
Dr. Kathleen Fisher (09:28):
And that wasn't enough to build really interesting applications. They could do some marketing applications, but they didn't really wanna do market applications. They really wanted to do fraud applications and they had to work super hard on the performance. So they really didn't, they didn't wanna be working on performance. They really wanted to be working on statistical modeling. They were really data scientists and they were having to spend all their time doing systems level programming. And this was like a, a skill and interest mismatch and what my colleague and Rogers and I did was we came and said like, we can build a programming language for you, where you can express the ideas at the level that you wanna talk about the ideas, about what information do you wanna store per customer? And you can write down the program at that per customer level. And then we'll take that per customer level information.
Dr. Kathleen Fisher (10:13):
And we'll compile it down to the per that does all the low level systems programming to pull in all those phone calls and do all the, the bit level manipulations to get the efficient enough program out so that you can process all those phone calls and, and push all the data through the diss to get out good enough performance. So that instead of doing two bytes per customer, you can do 120 bytes per customer. And that like sub orders of magnitude increase in what you could do, just like hugely open the flood gates in terms of what kinds of applications that they could do it saved at. And T hundreds of millions of dollars a year. It opened up tons of fraud applications. So yeah, at T was like, ah, now we know why we have language people, right. They, they went from like, what are you doing here to like, ah, now we know what you're doing here. And yeah, it was hugely. And the, when we talked to the, these data analysts and they, they saw their, um, their programs written in our brand new language when it was just like mocked up, it was just Ky, right. There was no language yet, but they like, they saw it as a language like, yes, that's the program we wanted to write. That aha moment was super satisfying.
Joey (11:16):
Yeah. Is a something, something I, I guess weird, like this is gonna sound insane when I say it, something kind of clicked with me as you were saying that, which is like, I, I feel like for a long time, when I hear I've heard domain specific language, I've like heard language, like is, is the, the bit that looms large and like separately, I feel like I've had, like on the podcast, we've had insights of like, you have to be really domain specific in your, and like, one of the things that struck me out of that description was like a lot of the real value was, was not even the fact that it was a language, but the fact that you understood the particulars of the problem, you understood what needed to happen, um, what there was missing knowledge between, it sounds like the data scientists and the computers and the, the, the value, like, yes, it was great that it was a language, the value was packing the automation of, of understanding the problem in so that those people didn't have to reason about that. Absolutely.
Dr. Kathleen Fisher (12:07):
Um, that's really cool. Yep. That was, it was called Hancock and, uh, Karina Cortez and Dar were the data analyst who worked with us on that, that problem. Uh, it was a lot of fun. We really, I really enjoyed working on that project.
Shpat (12:20):
What's interesting is often it's very hard to introduce a new thing in somebody's workflow. Um, what was it that made this just like, this is a no brainer we're gonna use this immediately. Was it just the, the, the gains that were gotten by using were just, you know, hard to ignore. Um, you've been, you've touched a lot of DSLs being worked on and some are more what languages in general, some are more, uh, uh, adopted than others. What made this one so successful?
Dr. Kathleen Fisher (12:46):
Indeed. Um, so a couple things, I think that the main one was that, um, the demand for the data that they were producing was off the charts. Like they had customers on the business side who were loving the data, they were producing, like the demand for the kind of information they were like, this was the beginning of kind of the data science revolution, right? This is like the very baby steps of the data science revolution. And you could just see the immense value that this data was already producing. Like the clearly hugely off the charge value. So the market was absolutely there, but the tools that they had to produce, it were excruciatingly painful to use to the point where they're like, we're not doing this anymore. Right. Like unwilling to, to do this. And we came and said like, here's a tool that you will be, you know, they were happy to use, like was so much better for them to use.
Dr. Kathleen Fisher (13:35):
So it's like they could continue to feed their customer base, who was delighted with what they were producing in a way that was orders of magnitude, less painful for them to do where they didn't have to do the parts of the job that they hated. And they got to do the parts of the job that they loved in exchange for tremendous downstream rewards. Right. So basically we provided a, a so solution for a D you know, problem that they desperately had at exactly the right moment. Right. If, if we hadn't come in, probably somebody, some other solution would've come in at the same time, or it would've died because they would've just said, like, we know you really like this data. We just can't do it anymore. Like, you can keep doing this one thing, but we're not gonna innovate anymore. And, and somebody else would've done something somewhere else. So it's the right place at the right time. Well, right. With the right tool.
Shpat (14:20):
Yeah. I was gonna say it's so it's easy. You just make people's jobs easier, uh, make their impact like 10 X and increase joy at work.
Joey (14:28):
Yeah. I mean, the, that makes it sound like it was really specific good luck. But I think the reality is there's a lot of right place, right. To times sort of available, you know, at the taking at any given moment. And it, it does take insight to discover those and to take advantage of 'em cuz like any software engineer you're gonna talk to is gonna have 50 things about their job. That's like way too hard and, and the farther you get away from a software engineer. So if you look like towards data scientists, um, you know, we see a lot of like in finance, there's a lot of people that, that understand the way finance works and need to explain that to computers. But
Dr. Kathleen Fisher (15:28):
I mean, another thing here that was really helpful was that the, the down stream customers, all they needed was the data and they could get the data through a web interface, right? The people that were using the language, they were other researchers, they were the data scientists. So in terms of the number of people who needed to adopt the domain specific language, we only had to sell a relatively small number of people on the domain specific language. Then they could use the specific language to feed a data interface that could feed, you know, lots and lots and lots of other people. So the, the DSL only needed to sell a small number of people to then be able to, to service a large number of people. Cuz it a DSL is, is a hard thing to sell. Languages are a hard thing to sell. Like it just like with people like, you know, human language competing languages are very difficult to learn they're they affect the way you think it's just, it's, it's a hard thing to introduce into somebody's tool chain, a language, whereas, you know, a web interface point your browser at a different URL, no big deal, right?
Dr. Kathleen Fisher (16:26):
It's it's, it's a much lower barrier to entry. So in this project we had a web, we had a, we only have had to sell a small number of people who were the ones who were in agony
Joey (16:45):
And I think for that reason, one of the, one of the shifts we're seeing, and I, and I don't know if anybody knows how to make the decision right yet is when do I use a DSL versus an API? Because now, now APIs feel like a, an easier way to sort of plug into what, what people already understand. Right? Like I, I already know how to use Python. So like if I'm just, if I can do more by calling different functions and Python, that's gonna be easier than learning a new syntax. Um, regardless, it seems like there's still applic where the DSL is the right choice. And I, I'm not sure it's so obvious when, when to pick, which, um, I think people have examples of really, you know, really well implemented APIs and really well implemented DSLs. But I, it upfront, I I'm curious if you have any insight into, to when you'd look for one versus the other.
Dr. Kathleen Fisher (17:32):
Yeah. I mean, it's a complicated design, right? So, so one is, if, if one of the powers of the DS of the design is you have less power. Like your, your DSL is not turning complete and, or is restricted and therefore you, um, uh, can reason about it more effectively then you can't be an API of a language that is turning complete and has all these bells and whistles because you, you can't, you can't throw away this extra stuff. Right. So, you know, if the power of the DSL is by being very carefully subset of something, then you need to be a subset. Also the type system makes a big difference, right? If you're, if you're leveraging a type system, then you can't be an API of Java. I mean, Java of JavaScript, right. Uh, or Python. Right. So that makes a difference to, um, also like one of the benefits of this DSL that I developed for, uh, at, at T was it provided the, the computational model, right?
Dr. Kathleen Fisher (18:32):
You as the user kind of slotted in the various pieces. So it was the driver
Dr. Kathleen Fisher (19:26):
Um, the reasons why you might prefer an API for all the reasons that you say, right, if fits within a tool chain, you get all of the benefits of the library that you already understand. Like the syntax is familiar. Um, so like basically if there isn't a super compelling reason to make it a DSL, you should make it an API. Cause you're not gonna be able to convince people to use a DSL. Even if you have unbelievably compelling reasons to make it a DSL, you probably will have more success with an API because of the inertia.
Shpat (19:55):
You mentioned pads. I've heard about that a lot. I did not know you worked on it. Uh, just out of curiosity, I would, I would love to hear what, when you worked on it and what, what it is.
Dr. Kathleen Fisher (20:04):
Sure. So I started the pads project, um, when I was at, at and T after the DSL that I was talking about before college Hancock, um, it started out of the, by analyzing the Hancock project about like, what is still hard about writing these signature programs and the, the biggest pain point was the input piece. When you describe the data that was coming in, writing that description just seemed like way too hard. Like you should be able to just declaratively specify the data. And one of the things that was really hard about it was the data never actually matched the specification. Right? You had an idea of what the data was supposed to be like, but the data never, it always had exceptions. Um, and so I wanted a way of writing down the data as it was, as you sort of understood it was supposed to be, but then you would, when you parsed it, it would not stop when it came to data that didn't match. It would just, it would return, um, a pair of the best understanding of the data as it could be. And metadata that described where the data didn't actually conform to that. Um, um, yeah, and we created versions of pads that were, the host language was C was ML and was, uh, was, has, yeah, I've had a lot of fun with the pads project over the, over the years. It's still kind of alive actually.
Shpat (21:20):
Cool. We'll make sure to link to it.
Dr. Kathleen Fisher (21:21):
One of the pieces we did with it was in fact, um, you have a lot of data. Can you just learn a pads from the data instead of making a person write it from hand? So we, we wrote a pople paper called from dirt to shovels. Basically you start with the, the data, which is the dirt and you produce useful tools for manipulating the, the dirt just from the dirt itself. And you know, the cool thing is, you know, obviously you can't do this all the time. If you have an adversary, who's creating the description, the data, then it's hopeless, but most data isn't created by an adversary. Um, it's just created by a semi clueless person. And so a lot of the times you can infer a description that's perfectly reasonable. You can infer the names of the data very well, but you can infer the, the structure reasonably
Shpat (22:01):
Well. I'm gonna just a side note. I'm gonna take semi clueless person and put it on my business card.
Joey (22:07):
That's, that's a good, good one. I mean, if you're professionally aware that you are semi clueless, that can be a strength amount of weak weakness, I'll take it as long as you're honest about where you're clueless and where you're not. So if I've inferred a pad specification for some data, what tools does that? Does that give me exactly what can I, what can I do then?
Dr. Kathleen Fisher (22:26):
So from the pads description, it will generate a data structure that represents the in-memory representation of the data that's isomorphic to the description. So it's not generic, it's, it's isomorphic to the description and then a, uh, a data structure that Des, um, describes kind of the, the errors that could occur in the, as you parse it. And then you get a, a parser that takes a, a bite string or a, a buffer, and produces that in memory representation, a, a pretty printer that goes the other way around. Um, and we formalized it, um, in the next 700 data description, languages, paper, and proved that you get kind of the round tripping properties that you would expect. Although those round tripping properties are more complicated than you might naively think at first because of white space kinds of issues, uh, white space is you think like white space seems so trivial, but in fact, white space is ridiculously complicated.
Dr. Kathleen Fisher (23:20):
So you, anyway, you get AF you know, if you think about it for a little, get, you get the, the round tripping properties that are the best that you could hope for, you get a statistical, uh, accumulator program, which lets you, um, read in often these kinds of data are sequences of records. And you can basically read in these, uh, records one at a time and build up kind of a bird's eye view of the, the records kind of which parts of the records are populated. This was very useful at, at and T for when you get a new data feed quickly understanding what parts of the data feed are interesting, and which ones are boring. Like is the data kind of uniformly, you know, is a field uniformly spread like lots of different values or is it like not populated at all? Or is it only really how, even though it's like an integer, it really only has two different values.
Dr. Kathleen Fisher (24:08):
Um, how many of the values are error or is it all error or is it no errors? Is it like, it says it's an integer, but it's really, it's an integer or it's a dash or, you know, things like that. This accumulator tool gives you a really nice, very quick, like you don't have to write any code. It just gives you back a, um, a bird's eye view of the data. And in fact, it, it will generate an application for you. You just write the description and you can generate an application that will run over the data and give you back a report about here's what your data looks like. It gives you a tool to convert to XML. It gives you a tool. Now it would be JSON, but back then it was XML. Um, it gives you a tool to convert to a relational form.
Dr. Kathleen Fisher (24:42):
And we talked about building a tool to do a visual, uh, of the data, but we never, we haven't yet probably this point won't, but that's an obvious thing to do. So we started using like techniques from type directed programming to use the type structure of the pads description to, to automatically generate type directed tools that work over. So you could write a, a tool that would be generic over the type structure, and then be instant for a specific pad's description to instantiate that kind of tool for that particular pad's description. So it was a great matching up of type directed programming techniques with the domain specific language to create a whole bunch of tools for manipulating ad hoc data sources.
Joey (25:22):
So it doesn't sound like you get very much at the end of the day.
Dr. Kathleen Fisher (25:24):
No, no. And it also serves a target for this, uh, format inference problem, right? So given raw data, it can start to infer data descriptions, um, and then you can edit them. Um, and we also started working on, uh, with Sam Kher, who is at, uh, alwa on, um, generating synthetic data that matches a pads description, according to, uh, probability distributions. Like we wanna have data that matches this in this field. We wanna have using a uniform distribution in that field. We wanna have a normal distribution in that field. We wanna have a press on distribution, um, to get data to, you know, to test systems. I think there's a lot more that one could do there. Um, I don't think it's a research problem so much as a, um, an engineering problem, but I think it, you know, is really useful engineering problem of,
Joey (26:08):
So basically you can go from, yeah, just a data set, like a, a whole bunch of data. It sounds like you can go from that, learn a spec, and then all these tools pop out these
Dr. Kathleen Fisher (26:24):
Of, yeah, maybe it's, uh, from dirt to Swiss army knives.
Joey (26:28):
I guess Kathleen, I think the first time we met and, and maybe I'm maybe you don't remember, this was, um, was during the HACCMS project, you did a, you did a site visit while I was a PhD student and I got to give a, I had to give a little presentation of what we were working on. And that was, was actually that meant a lot to me, um, to like, cuz that was a big deal. Like we didn't do a lot of external sort of client facing stuff. So that was, that was pretty exciting. And we got to do some really cool research on, on hacks, which was a wonderful program. Um, do you wanna tell us at, at a high level, what, what hacks was all about?
Dr. Kathleen Fisher (26:59):
Sure. So hacks was about producing software for vehicles that would be, um, demonstrably harder for hackers to break into and take over control remotely. So the threat model. So the, the platform that we were interested in was, was vehicles kind of as a proxy for cyber physical systems, things that were controlled by computers, but that could interact with the real world. Uh, the threat model was remote access because remote access is where you can have threats at distance and scale. So you can have a hacker on one part of, you know, one part of the country or one part of the world, remote hacking into a whole fleet of automobiles or other kinds of vehicles and causing havoc or, or D damage. It's not that there aren't other threat models that aren't also serious. Um, but you can only do so much. And we also only cared about the, uh, we were only focusing on the software.
Dr. Kathleen Fisher (27:53):
Again, hardware definitely has vulnerabilities, but you can only do so much of the time. So we were focusing on the, the software, we focused on, uh, actual vehicle platforms to get of concreteness to what we were doing. So we had two different teams. There was a ground team and an air team. The ground team was working on an automobile and a ground robot. And the air team was working on Boeing's unmanned little bird, which was a helicopter that was big enough to have two pilots, but could also fly completely autonomously. And then a, the RJ copter quad cop, which is, uh, off the shelf quad cop that you could buy from Amazon that can fly completely autonomously, um, that had about maybe a hun, you know, a hundred thousand lines of source code total completely open source. So like the idea here was that the, the ground robot and the quad cop were unrestricted.
Dr. Kathleen Fisher (28:46):
Everybody could see all the source code, no restrictions, uh, relatively simple systems, whereas the helicopter and the, the automobile and helicopter, those were, you know, proprietary, ITAR restricted, only the kind of vehicle expert had access to the code so that the, the blue team, the, the formal methods researcher, experts could work on the, the ground robot and the quad cap, try out their ideas in the context of those systems, um, develop them out and then transfer their ideas to the vehicle experts who could then try them out experiment with them on the, the bigger systems. And there was also a red team who's expertise was in penetration testing. And the red team at the very beginning of the program, tried to wirelessly remotely break into all four systems, uh, to provide a baseline like maybe all four systems were already secure at the beginning of the program.
Dr. Kathleen Fisher (29:40):
And nobody had any work to do that was not the case. The red team showed that they could break in and wirelessly take over control of all four systems without, um, without really breaking a sweat. Uh, we didn't, you know, we weren't all surprised that that was the case for the, the quad cop, for example, where the threat model that the manufacturer was most worried about probably was the quad cop was flying in the, and no one could connect to it. Not that too many people could connect to it. The owners of the commercial vehicles, I think were a little bit more surprised that the quad that the red team didn't have to work a little bit harder to, to break in
Shpat (30:14):
The reason we're asking you about this, obviously just in case it escapes any, any Watchers or listeners is that you started HAACMS at at DARPA and it, and then subsequently ran it. And it had teams like a lot of our R and D teams from industry and from, uh, kind of applied labs and from universities. Um, so, so it was like, it is a big, a big, a big thing and a big deal. What would you say looking back, that's the biggest contribu, uh, from, from hacks and, and the folks who worked on it that stands out as like, you know, that seems to be significant, whether it's actually technological or more, you know, that, that we learn on how to do things in the future.
Dr. Kathleen Fisher (30:53):
Yeah. So I think their contributions on multiple different fronts, um, I think the, the biggest contribution I would say is DARPA's role is one of the, one of the ways of articulating what DARPA does is it takes technical risk off the table. And I think that Hack's biggest contribution in fact is doing that. So when I went to DARPA and said, we should run this program, you, the way a program gets started at DARPA is a program manager goes to what's called tech council, which is kind of heads of DARPA every Monday or many Mondays program managers go and they make a PowerPoint presentation, um, basically hour long presentation explaining kind of what they wanna do and why they wanna do it and why DARPA should do it and what resources it will take and how long it will take and how you'll measure progress.
Dr. Kathleen Fisher (31:41):
Um, so, you know, I asked for basically many million dollars to run hacks. And at the end of that time, they're like, yes, but, you know, there were people on tech council who were like, this is like, ridiculous. This is never gonna work. Like systems are way too complicated. You're never gonna be able to do this. And certainly the idea of, you know, formal methods, being able to prove realistic properties of realistic systems is something that many people have been skeptical of for a really long time. And with, with good reason, right? People in the formal methods community have been saying that you can use formal methods to verify properties of systems for like 50 years. And for most of that 50 years, the only systems you've been able to prove properties of have been really toy systems. Right? So going to DARPin saying like, no, we can do this for real now was perhaps audacious
Dr. Kathleen Fisher (32:28):
Um, but I had, you know, really great things to stand on, like SEO, four microkernel and comp, like both of those had already been verified. I was able to go to tech council and say like, these two things already exist. This is like basis for confidence that I'm not just like making stuff up. That, that there's a real reason to think that we could do this. So I think the biggest, so like the hope was that the hacks program could produce evidence so that in the future Pentagon procurement officers could write RFPs. That would say, you know, if you, you want to win this contract, you must produce a system that has a machine checked, proof of memory, safety of communication, integrity of, you know, this set of properties that are like the set of properties that the hacks performers did for the unmanned little bird, and then, you know, publish that RFP.
Dr. Kathleen Fisher (33:16):
And then when the defense contractors come and say, you see these requirements, you have to take these out because if you put these requirements in, nobody's gonna be able to bid on this and you want your fancy gizmo, right? If you want your fancy gizmo, you have to take things out. And then the procurement officer can say like, well, these grad students did it. Like if you're telling me these grad students can do it, and you're fancy engineers who charge this amount of money, can't do this. Like what's wrong with fancy engineers, right? So like that proof of concept that taking the risk off the table, I think the hacks researchers completely succeeded at doing that. In fact, they completely succeeded at doing that in phase one of the program, right? By the time they got to the end of the program, they did it on not one platform.
Dr. Kathleen Fisher (33:55):
They did it in like 10 different platforms and they did it. So convincingly on the UNLA middle bird, unmanned little bird that they allowed the red team to attack the unmanned little bird from on the platform in a partition, not wirelessly on the platform while the helicopter was in flight with the pest pilots on board, right. Like utterly convincing case. Right? So there were tons of technical innovations that happened in the hacks program, but that level of confidence on 10 different platforms to the point where like the test pilots lives were in, you know, were so confident that their lives were safe, that they were willing to do that test in flight that I think is the biggest accomplishment of the hacks program. So that the authorization act, the last two of them have explicitly directed the Pentagon to explore using hacks technology in future procurements, right?
Dr. Kathleen Fisher (34:47):
Like hacks is listed by name in the last two. Um, DCAS the I'm forgetting the acronym, the bill that pays for the Pentagon every year.
Dr. Kathleen Fisher (35:41):
Um, that means that it will be more possible for the medical device industry to develop the same kinds of capacity. And for the, uh, parts of Washington that are responsible for regulating medical devices to develop the same kinds of things. So that pacemakers and insulin pumps also start to acquire the same kinds of rules so that it's not just military kinds of devices, but also other kinds of cyber physical devices that end up having the same kinds of assurance. And these kinds of devices are ideally suited because there are lots of parts of them that they're complicated systems, but they're not on the order of 500 million lines of code or a hundred millions. Like there are lots of parts of them that are a hundred thousand lines of code or 50,000 lines. Like they're, they're small enough that you can wrap your head, like the formal methods can work, right.
Dr. Kathleen Fisher (36:31):
Or that they're, they're exquisite, like the parts of the system that you can carve out that this is the part that has to work properly of it. You know, if the bells and whistles don't work exactly right. It's okay. It doesn't work exactly right. Like the bells and whistles will go wrong, but the, the insulin will be delivered properly or the, you know, the shock to your heart will be delivered properly. Um, and, and I, I can sort of see a positive spiral where we develop the capacity and we extend it to more industries. Like that's sort of like the vision of what, what I want to happen out of, out of hacks. And I think so far, we're still spiraling on a positive, you know, in a positive path. And
Joey (37:05):
You didn't mention the, like the progress that was made on the research side, as, I mean, this, one of the really impressive bits of, of hacks is that I think it was a program that was, that really played to the different strengths of the teams that worked on it. You meant the teaming approach and having the open source and the closed, um, platforms, but, you know, also you, it seems to have been set up. So the academic teams were allowed to really push the envelope and, and try some really tough stuff that was, you know, maybe a little riskier on, on the end, but like, and that some of the more industrial teams really applied things and, and let you have these amazing demonstrations at the end of the day. And I think that was a really clever setup that that really seems to have let things push in both directions, right? Like, um, we saw, I think quite a few really high tier papers that were doing brand new stuff in this, in this field come out of the program, as well as the, the demonstrations and, and accomplishing both seems like a, a pretty impressive fee
Dr. Kathleen Fisher (38:00):
Indeed. That was intentionally the way I had set it up. So that, that would happen. Like a lot of the work on the verified software tool chain out of, out of Princeton was funded on this project. And it was really exciting and, and work on verifying concurrency, which remains a super hard problem. Um, but people are making progress on. Yeah. So it was, um, intentionally set up that way is kind of having a, a portfolio approach of different kinds of performers who are contributing in different kinds of ways. I was also really pleased that the kind of air team bid as a team. And so, uh, came in all working together already. And the ground team came in as a bunch of point solutions never really functioned super well as a team, but each kind of was like the best of a whole bunch of individual technologies as a result.
Dr. Kathleen Fisher (38:42):
And we could really see what each individual technology, what, how much it, that individual technology could, could do. And so didn't have to like, wasn't cons I wasn't constrained to have to pick a whole team. I could pick this approach and that approach and that approach as a result. And that was really exciting. Yeah. It's another really cool thing about DARPA, right? One of the, we had performers in Australia, for example, right. You're not constrained to pick only us teams, which is DARPA's very, um, very able to pursue its mission of detecting and creating strategic surprise where of her the best performers are for creating a detecting strategic surprise within very broad latitude. If we
Joey (39:20):
Come back to the, the idea of the spiral that you mentioned and sort of, um, I think getting this sort of approach to a place where things are, you know, things start feeding in where we start seeing investment, cuz you know, I think we've seen a lot of great work in this air area, but just the number of dollars that have gone into it are not
Dr. Kathleen Fisher (40:11):
Yeah. Good question. And I haven't spent a lot of time thinking about that recently. Um, you know, I, I think the, like just picking on interactive, the improves, I think the interfaces are still not very intuitive. It only really works well for the person who's actually using the interactive, the improver at the moment that they're using the, the improve, like the, the mental model of what's going on with the proof is not very translatable to, to other people. Um, I think some work on making that more translatable. I don't know what that looks like exactly. And more automation even in that process. And maybe that's more machine learning kind of like how proof's gone in the past. I, I, I don't, I don't know. I, I, it's not my area of expertise, but something about the usability of like either more automation so that fewer will have to do the part of interactive theory improving.
Dr. Kathleen Fisher (40:59):
But I, I suspect that's not the right answer. I think interactive theory improving is gonna continue to be a really important, I mean, I think both the fully automatic stuff is going to continue to be more and more important. So fully automatic is, is, will always be super important, but we're never going to be able to do everything fully, automatically. And so when it falls is out of fully automatic, we're gonna be in interactive theory, improving when we're in interactive theory, improving how do we maximize the information that the automatic tools got and provide that to whoever's doing the interactive theory improving and then how do we maximize the information visualization to the person or the team who's doing the interactive theory improving so that they are maximally effective in, in what they're doing. It sort of feels like, you know, like with interactive theory, improving is not very different from programming, right.
Dr. Kathleen Fisher (41:46):
But it feels like, you know, the, the state of support for interactive theory improving is like the state support for programming. Like when I was an undergrad, right. It's like, it feels like it's way, way, way in the dark ages compared to the state of support for programming. So I, I think a lot of kind of like taking lessons from software engineering and, and programming environments and, and taking those lessons into the interactive theory, improving that's that's part of it. I, I kind of think that some of the it's possible that with the cloud computing and like Amazon web services and the, and Azure on the Microsoft side where they have FinTech companies wanting to use and, and the government wanting to use their cloud infrastructure in a way that they're completely convinced that their part of the cloud is isolated from the rest of the infrastructure, that might be enough of a market to, um, I, don't the kind of tools that you, that GWA has been working on with Amazon web services, for example.
Dr. Kathleen Fisher (42:49):
So to really a hard, I don't know, there, there might not be a big enough market on the formal method side to produce those tools to a high enough level of support. There's kind of like, what's the balance between investing in the formal methods tools, how many people need to be expert at the formal methods tools to be able to get the software that needs to be verified to a high enough level to be usable. I don't know where the right trade off is. I'm sure that the, the support for formal methods tools will get better because it's not there yet. And people will, are keep, you know, it's getting better. Right. Um, you're more of an expert in this than I am. So I, I should ask you what, what you think the answer to this question is,
Joey (43:25):
Well, it's, we're not here to listen to me talk. It sounds like one of the concerns
Dr. Kathleen Fisher (43:29):
But I wanna know,
Joey (43:32):
It sounds like one of the concerns, uh, I think, and this is something we see. So I, I I'll, I'll I'll, um, I'll pile onto something you said as an answer. Um, demonstr ability is a really tough question. Right? And with hacks, we talked about, we put people on an airplane and let other people try to hack it. And that's a really tactile way to feel like these people have confidence in what and what they've developed, right. Someone can, someone can hear that story and say, whoa, those, those people really believed in what they'd done. But like, if I show my, you know, if I show my, my interactive theorem screen going green and the, the Q E D turns green, and I say, well, like, this means that it's good. Someone's gonna be like, yeah. Okay. Okay. Computer guy, like, I, I believe you, but like, how do we, how do we, how do we make it feel convincing?
Joey (44:19):
Um, and you know, we've seen articles in the past few years about like, oh, here's all the, here's all the formal method, you know, the formally verified systems, uh, here's all the formally verified systems that got hacked anyways. Right. And it's like, and, and sometimes people say, oh, well, that's like evidence that we shouldn't have bothered doing the thing in the first place. Um, so I think I like, and, and some of the answer is like, go, go tactile, right? Like, go show, show your confidence if you, if you have it, um, in a way that people can consume more easily. But the other question is like, how do we, how we move past that? Like, how do we get to the point where, where somebody can consume something and, and believe it. And I think that's what you're getting at a bit with, with what you were saying about the interactive provers is like, if, if you're not an interactive prover person, what does it, what does it mean to you? And then how, yeah. How do, how do we help people? How do we help the computers explain what's going on to people? And how do we help people assume that in a meaningful way, um, to understand what they're
Dr. Kathleen Fisher (45:13):
Getting. Right. I mean, like when I look at one of my student's proofs scripts and it's like, help, help auto help auto it's like, that's a proof
Joey (45:35):
And one of the, one of the, the things that I feel like we've been repeating over and over recently is sort of the idea of make easy things, easy and hard things hard. Um, when you take a PhD student and say, do this proof, like they'll push through the, the easy things being hard, right. That's, that's sort of a good ad student's job. Like, and everybody's aware of it. Like that's, they're, they're trying to figure out why it's hard and make it better. That's, it's, it's part of the job description. But if you take a software engineer, who's got 30 things to do in deliverables, and they have this like thing. That's like, I understand why this is right. And you're gonna ask me to spend how long, like typing, typing simple auto, simple auto, like, no, I'm not gonna do that. That's easy. The computer should be doing that. And so like getting to the point where it's like, I like the, the dream of interactive proving is like explaining the insight to the computer and the same way I would explain it to you. Like if we sat down and I said, here's why my program's right to you. And you're like, I get it. I understand it. That's the kind of conversation at the end of the day. You want to be having with the computer and, and right. There's no
Dr. Kathleen Fisher (46:35):
Question we're not there yet. Yeah. I wonder like how much of that is like, okay, take the natural language processing, convert it into like actual language and then UN you know, a formal model of the language, like how much of that part needs to be solved and then converting it into the actual objects of the proof. And then wonder how many pieces of that pipeline are hard problems that need to be
Joey (46:55):
Solved. And it's gonna take some really special researchers to answer it. I think because it's like so many formal methods, people see natural language processing and they're like, well, I hope someone else solves that problem. So, so, you know, there's gotta be people out there, but, but also these big programs, um, have the opportunity to bring groups together. And in ways that,
Dr. Kathleen Fisher (47:15):
How far do you think we are from being able to do that? I mean, is that like a 50 year from now? Or is it a five year from
Joey (47:21):
Now? I think it depends so heavily on the spiral and how it progresses. Right. I th the, the rate's gonna need to increase, but once I'm still optimistic that something's gonna catch
Dr. Kathleen Fisher (48:02):
I mean, one of the challenges of like the natural language processing stuff is like, those models have come a long way, but they're all statistical at this point, don't actually understand anything. Whereas this would require mapping the speech to actual models of what's going on in the, the improver. Right. It actually might be a really good test case of converting the statistical model to, uh, actual model of what's like mapping the sort of surface statistical understanding to a deep model understanding of what's going on. D does that make sense? What I was saying?
Joey (48:35):
Yeah. And the beauty of program proof is there's no, there's no uncertainty at the end of the day, either the proof goes through or it doesn't. Right. So if it doesn't work, you have to figure out why that's a challenge. But if it does work, you don't worry that maybe like you thought it worked and it didn't cuz the proof went through. Um, and as long as your statement makes sense, then that's like, you can be pretty certain about it. And it's a, it's a rare bit of certain, you know, I think that's what draws a lot of people to, to proofs and, and proving is like, it's so, so uncommon. We get to say like, yeah, that's done.
Shpat (49:16):
I wanted to change topics a little bit. Um, you worked a lot in the effort to increase diversity and inclusion in computer science. And for those who don't know, you were co-chair of the computering research Association's committee on the status of women, um, you cofounded sick plans, programming land, which mentoring workshop. My question is for, for people who maybe are in computer science. And don't think about that. And for people who think about that and say, yes, diversity inclusion is important obviously, and then, you know, is business as usual. What would you want them to think about? How should they be thinking about how should we all I'll be thinking about that?
Dr. Kathleen Fisher (49:53):
Right? So like I firmly believe that talent and computer science is actually kind of uniformly distributed across various population demographics. And I think that it's, uh, really important that we don't miss out on talent because we are pushing away or not attracting all of the people who are actually good at computer science. Um, because we are misguided in like, because our filter is wrong.
Dr. Kathleen Fisher (50:46):
And so we really, it behooves us to really open our filter and to figure out how to make it. So like anybody who has aptitude in computer science, which again, I believe is uniformly distributed, uh, across the different kinds of people into the field and, and make them feel welcome. And that's not an easy thing to do because, um, um, it's implicit bias is a real thing. It's like all of us have, like if you do take the studies that, you know, out of the lab at Harvard, like all of us are biased. You know, like those implicit biases are built on stereotypes that we probably evolved, you know, thousands, you know, you know, over millennia to make us be able to make decisions faster, which, you know, I, I, it all makes sense. But the encouraging thing is that, um, yes, we have implicit bias, but we can overcome implicit bias.
Dr. Kathleen Fisher (51:35):
Right? We don't have to be like, knowing that implicit bias exists, you don't have to make the snap decision. You can say like, oh right. This is a circumstance where implicit bias might have an effect. So I should use my conscious brain to over what my implicit bias system might say. When we make hiring decisions, we should put in place a criteria in advance instead of not having a criteria in advance, right. When we have a hiring pool, we should make sure that there are at least two women in the hiring pool. Like studies show that if you have one woman in the hiring pool, you never hire the woman. If you have two women in the hiring, you hire one of them, 50% of the time, right? They're like all sorts of things that you can, you can go like L read the literature, um, about women, about black people, about Hispanic people, about other kinds of people who are under, you know, historically underrepresented in computer science.
Dr. Kathleen Fisher (52:24):
And you can figure out like ways and techniques for overcoming implicit bias and other ways to create environments that are opening and inclusive. And you probably create an environment that might be less comfortable. That probably will be less comfortable, but that's okay. Like in the long run, we will be, um, create an environment that is more inclusive and we will be more creative and we will invent a future that works better for many more people. And I firmly believe we'll will be better people in the long run for it. We'll learn more and we will grow more. And if we're a little bit uncomfortable in the process, that's okay with me. I don't always does that make sense? Very much so. And, and I think, you know, I've been spending a ton of time in the last year reading, uh, after, you know, as part of the black lives matter movement.
Dr. Kathleen Fisher (53:09):
I, I know a lot and I still have a ton to learn, but learning a lot more about the black experience in America. Um, and systemic racism that I, um, I knew a little bit before, but I know a lot more now. And I would really encourage people to, to take some time to, to learn more about that. I think it's really easy for people from not from the black background in America, to not be aware of all of the ways in which, um, systemic racism did not end with slavery and the long term consequences of that go find facts and, and figure out what, you know, where, where you stand and then what you think should be done.
Joey (53:47):
Do you have any specific efforts or things that people can, can participate in that, that you have going on currently, or, or organizations that you know, are, are worth contributing to?
Dr. Kathleen Fisher (53:57):
Um, well certainly the, um, PLM which, you know, programming language, mentoring workshops, which going on, like, as we speak, uh, well going on right now at, at, uh, P L D I, um, but they, those mentoring workshops happen at all of the four CIG plan conferences, CRAW which was the computing research association committee on the status of women has since broadened its now widening the pipeline. It focuses not only on women, but populations that have been excluded historically from computer science. So African Americans, Hispanic, Pacific Islanders, all populations that have been historically excluded. Um, that's another organization that does tons of really good programs. They're, they're actually a ton of them. NSF runs these, um, broadening participation alliances that work on various aspects. That's another really good place to look for, uh, data driven and well evaluated programs that have scientific evaluation of what works and what doesn't work, really advancing the science of understanding what innovations work and what, what don't work for moving the needle.
Shpat (55:06):
I, I appreciate you sharing that with us. One of the worst parts of doing this podcast is, um, the interviews have to eventually end
Dr. Kathleen Fisher (55:21):
It was my pleasure too. I've uh, really enjoyed getting a chance to, to chat with you. Thank you for all the, the really interesting questions and, uh, answers. I get Joey to answer a few questions. That was, that was good.
Shpat (55:33):
Yeah, it worked out. All right. Well that was another episode of building better systems. Um, we'll see you next time.
Speaker 5 (55:47):