Jean Yang, Founder and CEO of Akita Software, walks us through what makes API analysis an effective approach to finding critical issues in your systems, and what it takes to get a new company started. As a bonus, you'll learn about what formal methods and fashion design have in common. This is part one of a two-part episode. Please make sure to check out part two.
Video of this podcast can be found on our Youtube channel.
Jean Yang: https://www.linkedin.com/in/jean-yang-96575030/
Akita Software: https://www.akitasoftware.com/
Galois, Inc.: https://galois.com/
Joey Dodds: https://galois.com/team/joey-dodds/
Shpat Morina: https://galois.com/team/shpat-morina/
Contact us: marketing@galois.com
Joey (00:00:00):
Hello, everyone. Welcome to the building better systems podcast, where we explore tools and approaches that make us more effective engineers and make our software safe and reliable. My name's Joey Dodds. I'm a researcher focusing on providing assurance for industrial systems.
Shpat (00:00:13):
and I'm Shpat Morina. Joey and I both work at the Galois. Galois is a research and development lab that focuses on high assurance systems development, more broadly, just hard problems in computer science.
Joey (00:00:29):
And today we're joined by Jean Yang. Jean is a, Jean has one of these resumes where if you made it up and then showed it to someone, they'd be like, you made that up. That is a, that is, that is the prototypical excellent, uh, PL researcher resume. I can't be real, but that's, Jean's resume even though that's Jean's resume and it's really impressive. It's not, it's not what, you know, what I find to be impressive about Jean.
Joey (00:00:52):
What I think is really amazing about Jean is that through all of that, um, she kept an incredible focus on the problems that were important to her and realized that that world was not the right world for her to be doing the work that mattered to her. And, uh, so today we're going to talk about, uh, you know, we're going to go over that with Jean and discuss what that work is and why it's so important and how she's starting to take a bite out of the huge problems that she's going after. Uh, thanks a lot for joining us, Jean.
Jean (00:01:16):
Yeah. Thank you, Joey. And yeah, thanks for the very kind intro.
Joey (00:01:21):
Yeah. Well I think you, I think you deserve it. Uh, so yeah, I wanted to start off by asking, you know, what is your approach to building better systems?
Jean (00:01:29):
Yeah, absolutely. So I am kind of a strange PL person because I'm maybe all PL people have these two parts of themselves. They have, um, you know, the very principled, how things should be the idealized platonic version of systems where, you know, I, um, I spent a summer programming in boogie, which is basically like Pascal with preconditions and post conditions. And I was like, Oh my God, I feel so clean. Now, this is how everyone should program every day. It's the equivalent of like waking up like flossing twice a day, brushing your teeth after every time you eat and just like living this like pristine, perfect life. And then there's this other side of me. And I was just like, look, we got to get shit done. And so, um, I have a blog post, I think from 2013 where I talk about how I'm.
Jean (00:02:11):
So for my PhD, I, um, I made this, uh, domains, or I made this language for automatically enforcing privacy policies. And then I implemented it as a domain specific language. And in 2013 I switched that implementation to Python. And so I like, I don't know, like, so like what degree of PL nerd someone needs to be, to realize how far away from PL nerd Python is, but there's like, you know, your Haskell, your Idris, your like very nice, strongly statically typed languages and there's Python and Python is just like a very practical, dirty, um, there's like XKCD comic. You can just fly when you use Python. And, um, for me, I was just like, this is amazing. I can get stuff done. There are no guarantees. Language has no semantics that are documented that anyone knows, had definitely has no metatheory, but you can just get stuff done.
Jean (00:03:03):
And so I wrote this blog post in 2013 and that was like, I I'm using Python now guys. And I compared it to being like the vegetarian grad student who considers chicken a vegetable, because that's what they have at free lunch. But, you know, like on the one end, I think, I think, you know, I'd love to have guarantees for all of our systems. I would, um, I would love it if we like, you know, knew what was going on all the time. And, uh, on the other hand, I think we just need to ship lots of code into the world because that is how, that is how we make an impact. And so, um, a lot of my career has been trying to reconcile those two sides of myself, you know, how do we take these really nice ideas from formal methods and then bring them to the people who are like the other part of me, um, who are really passionate about just building stuff. Like if you asked me what I program it on weekends, it's Python guys. It's like, not even pipeline with classes. It's just like scripts. It's like, copy pasta, like me, like just like taking hard-coded bout like, you know, like there's like some stuff I'm just like, I've got 15 minutes. I need to get this done. And like, you know, it's, it's ugly. And I think that, um, I don't know, maybe other appeal people don't do that, but definitely I've never heard another appeal person really admit that.
Shpat (00:04:21):
I want to clarify when you say PL person is programming languages,
Jean (00:04:25):
Programming languages. Yeah.
Shpat (00:04:27):
So if I might recap your approach to building better systems sounds like it's focused, making sure that you're focused on the building.
Jean (00:04:35):
Yeah. I'm, I'm very interested in building and I want to make sure that no matter what kinds of tools we build, uh, for making the systems more robust for making them more secure for making sure that we actually know what's going on in the systems, we never leave behind the people who just want to build and who just want to build as quickly as possible because there's that there's always been that side of me.
Joey (00:05:00):
Yeah. I think that's great. I think it, and it's a, it's a really rare combination. Um, and you know, especially after you spend so much time in academia learning the ins and outs of so many of these really clean systems that, you know, they have, they feel great, right. Like you said. Yeah.
Jean (00:05:15):
And I was just like, you feel like you're going to go to software development, heaven or something, for sure. Yeah.
Joey (00:05:20):
You know, the problem you get it done. It's like, it's like, it's like, it's like problem sets kind of the, like you get to do that forever. And it keeps getting harder and harder, but like to go that deep into that world and still say, we got to stop, we've got to, we've got to figure out what of this can, you know, what, if this can crossover today? That that is that's hard, but it's really important.
Shpat (00:05:42):
often not always, but often when I talk to people that are kind of into Formal Methods and those things, sometimes these two worlds seem to be, um, uh, kind of incompatible
Shpat (00:05:58):
In terms of like, you know, if you're writing, if you're building stuff on with languages that don't necessarily provide some of those protections or don't allow you to, to apply some of the, some formal methods, then maybe some people will be like, well, are you really building, you know, systems that are better for, for some definition of a better, I'm just curious about like your, how you think about that.
Jean (00:06:21):
Yeah, no, that's a great question. And I think this yawning divide between formal methods and what people mostly use in practice is what I've been going after closing for my whole career. And here's the way I look at it. Um, so I, um, I first started thinking about this after junior year of college, when I took programming languages. Um, and I fell in love with functional and programming. I fell in love with semantics. I fell in love with types. And to me it was such a revelation that we could actually make sense of the mess that is software. And then I go off to Google and that summer they're rewriting the video search front end from Java back to C because they can't afford the 50% memory overhead. I try to strike up conversations with people about functional programming. I just get mocked. And, um, so I would write to my professor every week and be like, Hey man, you taught me some stuff, but it doesn't seem to be in practice here.
Jean (00:07:20):
And I'm, and I, and what I realized was a lot of the people who are working on this is how programming should be. Um, they were a ways away from the people working on what programming is. And, um, it was, you know, it's two different groups of people, two very different mentalities. Uh, but I think in the last years it's been closing a lot. .
Jean (00:08:05):
I think, I think that gap is closing. I also think that compute has become cheap enough that a lot of the software verification software analysis tools can actually be practical now and programs that are longer than 10 lines. Um, but I do think there's a huge remaining gap, which is most of the work and formal methods has been done assuming like a pretty monolithic, um, classically architected system where you, you know, you have your assembly, you model that assembly, you have your next level up language, you model that. And then like you kind of layer on top of that until you get to like your whole thing. And so if you're building like NASA spaceship software, like that's probably fine.
Jean (00:08:52):
They're probably still doing it that way. But if you look at modern web applications, Oh my God, you have this massive heterogeneity of the software environments that things are running in. You have this massive heterogeneity just like throughout the whole tech stack, you have, um, you know, uh, different language frameworks that everything is running in different kinds of machines. You're running in containers, you're running and all this stuff that how, how do people even model that? And then what's more is then you have everything talking to each other across the network with remote procedure calls. And so this, this is stuff that typically no one modeled cause we haven't gotten there yet. It's a combination of we haven't gotten there yet. And, uh, no, no one in, in academia is really programming systems that way and in programming languages. But to me, the really interesting question is how can we take ideas from formal methods and actually team this, this world.
Jean (00:09:48):
So massively multi-service massively heterogenic heterogeneous in terms of the tech stack and all of that. And how do we actually bring order to that? Yeah, that's a really good question. And so I, um, my view there is that we can still have formal models. We can still have nice guarantees, but we are not getting them by starting at the assembly. We have to start at a much higher level of abstraction and these specifications are not coming from programmers. They need to come some other way. And so, um, how, how a lot of modeling typically works is someone spends, you know, one to 20 years modeling x86. They're like, all right, guys, we've got this, this model of vaccine 86. Now let's model the next level up. And let's, you know, let's, let's go one layer up at a time. And, um, how, um, how I think we really need to handle things in this new world is we, um, so I I'm really in love with the API layer.
Jean (00:10:49):
So I think that, um, you know, all of these massively multi-service things there's, there's APIs that they call each other from that is clean that's well defined. Everyone has them. We should really start thinking about that. Um, not, not the applications inside, but really that's the layer of obstruction. That's really interesting to me if we're, if we're talking about these, these ecosystems of software here, um, and how we're getting specifications and any kind of model there can't be from programmers, but we need to get them from some kind of software analysis and the software analysis that we have there is also going to be nonstandard because no, one's really been trying to do that at scale, um, at all, but sorry about this. Um, here, let me just actually put this over here. Um, okay. There we go. Sorry. Uh, but, but yeah, I think the API layer is really interesting for this reason. Um, and I think how we're going to get ordered to the API layer is software analysis tool. So I'm really excited about black box analysis tools like fuzzing, um, things like quick check, quick check, or a Benjamin Pierce has this latest one that where he even like, it's some other thing and then chick, but you know, it really evolves, but, but things that, um, take software, treat it as a black box and then try to shake guarantees o ut of it, um, by, um, by, by testing and other kinds of non traditional formal methods approaches.
Joey (00:12:14):
So I wanna, I want to ask you a little bit about, you know, you said like maybe these things can't come from programmers and I I'd say maybe I'm not so pessimistic about that. And that like, when we're doing API work, the pro programmers like programmers have to communicate each other with each other often across companies around what their APIs are. So is there, is there a good reason to believe that we can't rely on programmers or is this just about making it as easy as possible?
Jean (00:12:42):
Um, I think there's a, it's a combination of the two. Um, I think, uh, to me, one of my guiding principles with everything I do is try to make things as easy as possible because people will always do the easiest thing. And I think that, um, in the beginning of the Akita journey, so, um, we're not, we're not saying very much publicly about what we do yet, but, um, so far I've revealed it's about API APIs. There's something,
Joey (00:13:03):
what is Akita?
Jean (00:13:05):
Akita is my company. Um, and, um, yeah, so we're still, we're still a technically a stealth mode startup. So, um, what, what we reveal is we do something around APIs. We do something around a black box software analysis. Um, and, um, in the beginning of the journey I went in with a much more strong assumptions about people's, uh, willingness to document and, uh, their knowledge of what was in their system already. So in, in the very beginning I went to people and I said, okay, so you want to enforce policies on your data. Cool. I can help you do that. And they said, wait, wait, we don't know where we have data. We don't know where the data's going. We don't know what software touches that data. And so then I thought to myself, okay, we need to take a step back. Um, and that, that's how we started doing a lot of the work we're doing around, uh, taking software, uh, taking it in a black box way and telling you this is what's going on.
Jean (00:14:05):
Um, and then the next step was, we said, okay, well, as long as you have an API and you know what that API is doing, we can tell you, this is where you have stuff coming in. This is where stuff goes out, here's where bad things might happen. And they said, that sounds great. But look, we don't even know what's going on with our API. And so then we had to take a further step back. And so that's when I realized man, um, should and, uh, should, could, and like the reality are very far apart, um, when it comes to software and I'm not blaming anybody, I think that's just how things go. Right? There's um, I should floss my teeth, uh, twice a day and then there's what I actually do. And then there's even, uh, how floss my teeth twice or once a day, but my dentist doesn't think I do. So, um, so I think it's, that's just the realities of life, you know, sometimes you have higher priorities.
Joey (00:15:01):
Yeah. That makes a lot of sense. So, so really, you know, and, and even if people are doing documentation, that'll only help the process,
Jean (00:15:09):
Right? Yeah, absolutely. So, yeah, what we've come across is, um, there has been one company with really good documentation. Um, I won't say who they are, but they have pretty good documentation and they have, um, only pretty good documentation, I think, on their external facing APIs, um, their internal ones, I think it's, um, it's a, it's a big question, Mark. And I think a lot of companies, um, if you, if you think about a company that's moving fast, trying to ship stuff out, um, and the API documentation is not high priority, it's just not there. And then if you think about other other software quality things, like how many tests do they have, um, what are they actually doing? I think it's very far from the, the, the golden standards of, of the programming languages community.
Shpat (00:15:55):
I, I have a dumb, dumb, a dumb question, or maybe a clarification we're talking about modeling things, but maybe it's not so clear as to why. And how is that helpful in the grand scheme?
Jean (00:16:07):
That's a great question. So I think that, um, the, the reason of why that someone might actually care about is, um, uh, things like security, things like privacy, things like other catastrophic crashes that can, um, that can take down your system. Um,
Shpat (00:16:24):
Yeah, but so like, uh, you model it in order to do something with that model.
Jean (00:16:29):
Yeah. In order to make sure that a bad thing isn't going to happen. So for, for the whole, for the, for the whole field of programming languages research, I would characterize it as you model what's going on in your programs so that you can know certain catastrophic things don't happen. And so, um, for a lot of the classical work, it was about, you know, catastrophic, the, the Holy grail was like catastrophic, um, operating system crashes where if you had a, a space ship and it had an operating system, there would be nothing that would just like Explo this spaceship or something like that. So those are a lot of, um, the classical use cases when, um, when I became a grad student and I realized my interest was in building these kinds of building tools to give these kinds of guarantees at scale, I concluded that security and privacy was going to be the catastrophic place where that could happen, because if you have so, so the way I think about software, especially modern software is it's a big pile of bits.
Jean (00:17:28):
Like if you think about like back in the old days, read the books about, you know, early MIT, bell labs, hackers, their programs are like 20 lines long. There are these recipes, they're, they're like cooking recipes that people could share around, you know, they were not complicated, but now what software is, is it's this whole ecosystem. And so I described at one point as it's a whole rainforest, not a single tree. And so taking any piece out or putting any piece in can disturb the balance of the whole thing, but you don't really know what's going on. And so, um, so there, I would say, um, in, in a, in a, in a modern software system, things that really can bring the system to its knees are well, there's obviously things like, you know, just like huge outages where there's like a bug that takes the whole system down.
Jean (00:18:13):
That's not what I work on, but that, that is one reason people model. And then the kinds of things I'm interested in are, does data go where it should and does data go, uh, not go where it shouldn't? So a lot of these things like these big breaches and these big, um, hacks, um, part of it is like, well, the hackers hackers are gonna hack. There's always going to be hackers that, you know, find ways to break into your system. Um, but the other reason this happens is there's just so many components in your software and no one really knows where data goes. And so a lot of the existing solutions are like, let's inventory, all of our databases, and let's crawl all over databases. Let's look in there and make sure that, you know, things are where they're supposed to be. But, um, you guys might be very sympathetic to my view, which is there's this whole pile of software that is moving data from one place to another. And if we can know what that does, we can shine a much better light on what's happening in our system with respect to these potentially catastrophic security and privacy issues.
Joey (00:19:17):
So really the kind of the kind of systems you're talking about, let's, let's like we'll dig into that kind of rainforest analogy a little more, what we're talking about. We're talking about tons of tons of programs, basically that are all running in different places in a network, and they're all talking to each other. And even the way that they're talking to each other might be changing day to day, is that kind of the situation that you're saying,
Jean (00:19:38):
I would say that's the, that's the extreme end of the scenario, but if we take a very basic system, so how I got into the problem is this way. So for my PhD, I did this, uh, new programming model for automatically enforcing, um, information flow security policies. So people in industry might just understand them as access policies or privacy policies. Um, the reason they're called information flow is because they're about data as it interacts with the program and not just, you know, data in a database or, um, or, or something like that. And, um, I implemented the language and then my advisor said, why don't we build some web apps to really demonstrate that this works. And, um, I'm hosting a conference in a couple of months. Why don't you just build a web app, um, use based in our language and host the conference using that.
Jean (00:20:24):
And I'm very quickly, I realized there was a big issue, which is you can have your language and your application layer, but in a basic model view controller system, your, your controller has to talk to your data models. And the minute you call outside of your application layer, what happens is all of the guarantees you got from your nice language level model are subverted, right? And so I had this nice language where you could attach policies about where data should go to the values themselves. So to like, if I have like a credit card and I'm only, I should be able to see it, I should be able to attach that data, a policy to the piece of data, wherever it goes in the program, uh, that policy follows it. But the problem was whenever I call it out to the database, there was no policy on the database.
Jean (00:21:14):
I could just do any database queries and, uh, you can get all kinds of information from the database and it completely breaks your thing. And, and it's, it's even more subtle than just like querying the database for your credit card. It could be like, let's say no, one's allowed to see my location. Um, but then I get, uh, I can query the database on all people who are in Redwood city right now, right. Then there's an implicit leak of my information from my location from that. And so there's just all kinds of problems when you go outside of your single application. And then if you think about what happens in your front end code, that again is a thing. So even, even before you have like this massive multi-service system, um, you get into some real issues with, uh, with like hetero heterogeneity and, um, calling across cross language. And then, um, what starts complicating it is the minute you start getting a, a multi-service environment, uh, you have those remote remote procedure calls. Um, every, every introduction to every information flow security paper that says, let's assume you have the system, you can call out to anything you don't know where it calls. That seemed very impractical when you had like a 10 line monolithic piece of code now becomes hugely relevant when you have this massive heterogeneous multi-service system.
Joey (00:22:35):
And so it sounds like the conclusion you really came to was that from inside of the system, at some point we just, we almost lose hope. Um, and that,
Jean (00:22:44):
Yeah, yeah, exactly. So I, I had, um, I had started, um, I had started my career saying, yeah, we're gonna tackle everything in the application level language itself. We're going to extend languages. We're gonna plug every hole. And I actually had this parallel line of research where, um, I had done this dynamic enforcement for information flow security policies for my PhD. And then I had worked with Nadia [inaudible] on a paper where, um, we did static enforcement of these policies and actually static synthesis. So we could insert access checks into your code from static checking. But we did this for liquid Haskell, which is a liquid refinement types on top of Haskell. This is extremely limited because Haskell first of all, makes extremely, uh, strong assumptions about what you have in your language and then liquid high school, further constraints that. And so then my next step was okay, we'll do it for JavaScript, Lakewood refine and types on top of JavaScript.
Jean (00:23:40):
And then again, it was very limited. So, so I had this parallel research track where I was like, okay, we're going to tackle everything about programming and we're going to handle, you know, dynamically typed modern languages. And we're going to do all this automatic enforcement and everything's going to work. And it was kind of like, I don't know if you've seen one of those scenes where someone's in a ship and just keeps having holes and they're plugging up all the holes. And I felt like man, like there was just always another case or there's just always something else to plug up. And so that that's really how I got obsessed with, um, the API layer, because to me it was a way to start fresh. It was a way to start clean because once you start getting into the game of taking every single programming language in the world, trying to clean it up so that you could put, you could enforce a thin level of guarantees on top of it. It just seems like, you know, not just one rat hole, but like 1 million rat holes. Uh, whereas if you can, um, if you can start one layer up, get clean guarantees from that, get, you know, block box, whatever you have in your application, meet those guarantees, have other models on top of that clean layer. Like that actually gives you hope of, of modeling this whole thing.
Joey (00:24:57):
Um, yeah. Have you done, have you done any one, one real challenge? I think so. So there's two challenges, right? One is one is what is your provider API providing? And is it, is it safe? And the other is if I'm someone calling an API, am I using that in a, in an inappropriate and safe fashion? Have you looked at both sides of that? Are you sort of,
Jean (00:25:18):
Yeah, so that's, that's a really good question. So what we're doing at the API layer is, um, we are providing tools to answer both of those questions. And so, um, so really, uh, I see the, the first step in cleaning anything up as a understanding. And so visibility is a term people like to use. What we're trying to do is give visibility to what's going on in your, in your software at your API level. So, um, so both things you said is, is the API you're, you're providing doing what you expect it to. And when I use another API, am I using that in a way that I expected to both of those are questions we're working on answering. And, um, it's still very much in line with my other, whereas my data going work. Um, I think in general, these are very hard questions to answer, but when it comes to, is my API giving back the data, I thought it was, am I, if, am I giving my data to this API in a way that I expect, or, you know, is it processing it in a way that I expect those are the kinds of questions we're answering?
Joey (00:26:19):
That's awesome. And so, so part of the goal is to part of the goal is to detect problems. And part of the goal sounds like it's just to explain to people what's going on with their system.
Jean (00:26:29):
Yeah, absolutely. And, um, I think that right now, when people think about API APIs or they think about data, they think of this as a very, very one dimensional in some way. Like when people think about data, they think about their database. And when people think API APIs, they think about, you know, the one layer that is their API. And so when people talk about, you know, data and access, they think about like, do I have like one thin layer of access control on top of my data, when they think about API security, they think about, you know, do I have the right token checking at my API security level? But to, to me, what's interesting is, uh, what's always been interesting is the interaction of data with the rest of your software. And so, um, when we say we're doing this, uh, at the API layer, that's, um, that's the entry point for all of our black box analysis, but, um, but we're doing much more than, you know, looking at the API functions themselves. We're looking at, okay. If we, if we, um, hit the software through this combination of API calls, what's happening, things like that. And not just, you know, is this one API call secure.
Joey (00:27:34):
So if we have anybody that's listening, that's not familiar with the concept of Blackbox. How would you, how would you explain that to them?
Jean (00:27:40):
Yeah. So there, um, there are many levels, I guess there's white box, gray blob, gray box and black box and white box is full access to source code. Uh, you can, you can see anything you want and you can analyze the code itself. Uh, block box is no access. So you, you, um, so it's the equivalent of, I don't know if you've ever had like a box of stuff in your house that you just keep moving from house to house because you packed it at some point. Um, you never really needed very much from it, but like keeps going with you and it's just part of your life. So it turns out a lot of software kind of is like that. Um, except people interact with that box and like they get stuff from it sometimes. And so, um, so that, um, that image is kind of what drove a lot of our desire to be fully Blackbox.
Jean (00:28:28):
So we want to be able to take your software, not really need to access the source source code, not need to understand what it does, but be able to poke at it and give you a summary of this is what you need to know about it. Um, because that, that seemed to me like a, a big part of how software development gets done is people are just carrying these boxes with them, um, for their whole lives and something like gray boxes in between. So it might be, um, you don't see the source code, but you get to instrument the code at the conditional branches. And so whenever a conditional branch gets triggered in the code, you get, you, you know, that that happens, but you don't see the whole code. Um, but yeah, I, I, my dream is for everything to be fully black box. Like we don't need to get in there. We can just wrap the code, be like, alright, we like, did these tests on it? And here here's what the code is doing. Here's what you need to know.
Joey (00:29:18):
And so when we look at, when we look at the trade offs are really the advantage you're seeing with black boxes that every, every system out, you know, we won't say every, but the vast majority of the systems out there are heterogeneous in the sense that, you know, like a bank for example, will have its core it's core program. Maybe it doesn't even have the source code for it anymore, and it's running at the center and then they, you know, the year they wrapped another layer around it and then they wrapped a web API around it. And then that one talks to another one black box, lets you treat it, lets you treat all those the same. You don't have to worry. And you just, you just go after them and figure out what they're doing.
Jean (00:29:54):
Yeah, absolutely. So, um, yeah, a big motivation for all. This is, um, I gave a, an industry talk in 2015 and um, it was about, uh, the main, the main thesis was there are all these great ideas we have in research. And I see you guys doing these practices and industry, how can we make it come together? And um, someone came up to me after the talk and they said, you know, gene, that was super interesting, but I mean, how do we get from where we are now to this world you're talking about? And then I dug in a little more and somebody else said, well, you know, a lot of what you programming languages, people do is the equivalent of us going to the doctor and the doctor saying, well, if he had just eaten an Apple every day and uh, floss your teeth and all these other things and you wouldn't be in this position, so why don't you just start over what everyone tells me is, well, we can start over.
Jean (00:30:46):
We already have all this legacy code. And even if we started over, we need some way to interact back with that. And so even if, if starting tomorrow there was major unification of languages out there. It is, as you say, there's stuff that people built before. It's hugely fragmented. It's always going to be there. And then it's not just languages at the application layer. Right. But if you think about data stores as their own runtime and you think about front ends as having their own runtime, like the Dom, um, I've also done some work on information flow across, you know, the Dom and the backend and things like that. Um, and so you just have, you just have a lot of components, no matter what. And if you're going to innovate in your tech stacks, there's just going to be more components it's not getting better.
Joey (00:31:31):
And you know, that that w will, will represent the other side of the trade off. Although it kind of obviously doesn't apply to the problem that you're trying to solve, which is that a lot of times there is source code around and there's a lot we can learn from the source code.
Jean (00:31:42):
Yeah, yeah, absolutely. Yeah. I think that, um, when you have the source code, it's a, it's a much cleaner and more principle problem. And in a lot of ways you have to just kind of cowboy your way through 'em if you don't have access to the source code. Um, but, but yeah, I think that, um, since my goal is let's, um, let's try to tackle as much surface area as possible, um, as quickly as possible. That's how I came upon this view.
Joey (00:32:08):
I was going to go back to something I heard you say earlier, which it sounded like a, of a personal philosophy that I, that I wanted to dig into as you, you kind of said, uh, uh, get shit done. Is that like a, is that like a thing you do? Like sometimes, um, you know, I think let's see, this is, this is going a bit into work style and out of formal methods, but like you've started a company, right? Like you have, like, did you just go do that? Like you just woke up one day and said, I'm going to, I'm going to do a company.
Jean (00:33:07):
Well, it was a series of events that led to the company starting, but people tell me everything is caused by a series of events, but, uh, essentially what happened was, um, well I think, I think for me, yeah, I, I, I mostly, um, I commit to things very quickly, um, after thinking about them very fast. Um, and then I follow through and so that's, that's kind of how it happened. So, um, it was, uh, early, early 2018. Um, I got, uh, an invitation to speak at Davos at the world economic forum and which was, which was very cool. It was, it was a great opportunity. And there, I got the chance to talk to a lot of C level executives from different companies and, um, for my whole career up until then, like nobody cared about cybersecurity and absolutely nobody cared about privacy because when I started my PhD, people would say things like, Oh, that's interesting.
Jean (00:33:58):
How did you pick privacy? Is Facebook going to matter in 10 years? Who's going, isn't privacy just going away. And so, um, I, I had kind of, my bet was in 10 years, people are gonna care about this and that, that was 2008. And so, um, so, you know, everyone has those things they say, so you don't really think they're going to come true. But, um, here I was, it was 2018 and I was talking and even cyber security, you know, before that people were like, huh, like, does, does that even matter? And I hear I was in 2018 and talking to these C level people and they all said what you do cybersecurity that is very important these days. And this just, you know, this, this blew my mind. And then they said, have you looked at GDPR because this was in Europe, there are a lot of European executives.
Jean (00:34:42):
And they said, well, you know, we really need to know where our data goes in our software now. And I was just like, what is going on? And so this, you know, this was such a, a different, uh, a different, uh, ambiance than I had ever existed before that I, I felt it was very important to take note. Um, but I think that, so that was kind of the, the proximal, uh, trigger for all this. But I think for, for a very long time, I sort of concluded that, um, for some of the impact I wanted to make, uh, in, in technology, I would probably want to start a company at some point. So in the early 2010s, I got very interested in entrepreneurship. I, I spent a lot of time looking at other, other kinds of, to other tech transfer stories. Um, I concluded that, you know, the one kind of tech transfer I could do is based on the work that I actually know and care about.
Jean (00:35:34):
Um, and so I concluded at some point that, you know, if I started company, it would have to be very much around program. It lists software tools, programming, um, guarantees, things like that. And in 2015, um, I actually started an accelerator with my friend because I was like, well, if I'm going to do this one day, I have to know what it means. And so, um, we got a VC firm to give us some money and commit to giving us office space where we picked, uh, we sourced teams, uh, in the cybersecurity space. Initially it was cybersecurity research like PhD kind of people. And then they would give 'em initial funding and office space and, um, and you know, the network to help them. And so then I learned, okay, if I want to do something in the cybersecurity space, it has to be, um, it has to be tied to regulatory shift because nobody cares about security otherwise.
Jean (00:36:21):
And, um, ideally it has to be tied to some kind of technological shift where people are looking for new tooling anyway. And so that kind of set the scene for, um, in prime me for 2018 when I realized, Oh my God, there's this major regulatory shift that's happening. I should really look into this. And so at that point, I was two years into my tenure track position at Carnegie Mellon. Um, it's not really the time you just, you know, take a sabbatical, like you don't get a sabbatical two years in, um, you also don't have a lot of momentum. So I had just raised like a couple million dollars, um, where I was the lead PI on those grants. Like it was a lot of work to get that money. I had just recruited some students and postdocs. It was really not a decision I took lightly.
Jean (00:37:03):
Um, because I recognize at that point, if you take a leave, you're pretty much winding down your entire momentum. Um, it's, it's pretty much like you're leaving academia. So then I was like, okay, this is a big decision. But if it's an even bigger opportunity to actually start my company at this point, then I have to take that. So then I spent that spring kind of going through my entire LinkedIn, calling everybody who would take a call from me and asking them what they're doing with their data, what their software situation is, and really assessing the situation. Um, mid-spring I had gotten enough confidence that I filed for leave. At which point I decided it was irresponsible not to tell my students. I was like, Hey guys, I'm thinking about doing this. You should probably figure out a co-advising situation. Um, let's, let's make sure you're okay.
Jean (00:37:46):
And, um, then when you file for Lee, if you, you know, you have to switch over your teaching requirements of the fall and all that stuff. So then by the time you file for leave, you you're pretty much committed to taking a leave. Um, whether or not they approve it, if you, if you go about it responsibly. And so then I was like, well, all right, I have no job in the fall, so I should probably give up my apartment. Um, and so I convinced my friend to take my apartment, and then I had nowhere to put my furniture. So I had to sell him my furniture as well. And so at one point it wasn't that I had committed to doing the company, but in order to make it so that I could do the company, I had nothing left. I had no group, I had no house, I had no furniture.
Jean (00:38:26):
And so, um, it was I'm in some ways it was the easiest, easiest decision I've ever made. Cause I think the worst kind of decision is, um, one you make too quickly and then you were grow up, you regret it or one, that's not really like a firm decision where you're like, alright, I'm like halfway doing this company. And I'm halfway, you know, doing this professor job. But for me, I was like, well, I can't do it in Pittsburgh because there are no, there's not enough customers here. And I can't do it at the same time as running a group because my group is not far along enough. Cause like I was spending, you know, 300% of my time on my CMU job. There's no way I could have kept that momentum going like that early into a tenure track job. Um, so it was, um, I was forced into a series of decisions that made the ultimate decision very easy and in some way,
Joey (00:39:11):
But it sounds like it was a path you put yourself on a, you know, that's a micro version of that is like with this podcast, we just started going out and doing interviews. Cause I wanted to put our, you know, I wanted to put us in the situation where it's like, if we don't, if we don't get this episode done, we're going to, we're going to let Jean down. We're going to let all these other people.
Jean (00:39:29):
No, it's it's yeah. It's one of those things where you're like, alright, I'm going to do this next thing cause I want to, and then you were like, yup. There's no, there's no going back now. Um, so I think at every point it was, it was like, let's do it. And then at the end it was like, here I am.
Joey (00:39:42):
Yeah. It's, it's great to play these tricks on yourself where you're like, you know what, I'm just going to take this like easy step, but that's going to kind of force the hard step event. Like we know we know what the end game is here. Right.
Joey (00:40:31):
one of, one of the limitations I see in, you know, the, that I'm a bit envious of you, although, you know, you've, you've earned this through hard work is basically like exposing yourself to lots of, lots of problems basically. it's, it's really hard to reach out to like this, uh, this, this going after your entire LinkedIn network thing, like you made it sound like, Oh yeah, like it's just something you do. But like that is, that is hard. Like it's hard to start so many of these conversations, it's hard to ask people for things. Um, and then, you know, it's like, you have to wrap your head, your head around like all these different problems that people come at from different ways. It's uh it's but like in the end, I, it seems like it's really crystallized your idea of what, of what need to do.
Jean (00:41:34):
Yeah. Well, I think we're still, we're still testing and iterating, but I think, yeah, the product work that we've been doing has really been helpful. And, um, to be very honest, you had a question in the doc about, you know, what's, what's the reason you're doing this in a company rather than academia. And I think my short answer is the product work and the user research and, um, all of the things where I'm in a paper, it's like two paragraphs of your introduction or it's in the, you know, two, two sentences of your, the impact of this and your conclusion. But I think that like that work to me is really satisfying to be able to actually justify this as who's gonna use it. Um, and I think you guys at Gallo actually, I've been envious of your stuff for a long time. Cause you get, you know, real contracts with people with real problems and then you guys get to do like the really cool technical stuff.
Jean (00:42:23):
I think that's an awesome model. Um, and I think for me the kind of problems I was always interested in this, like, you know, at scale thing, I was like, well, you kind of have to talk to a lot of people to understand those problems at scale. No one's coming to you with a big contract. Like, Hey, every developer in the world banded together and they're all chipping in 2 cents. So here you go. But dollar Kickstarter. Yeah. Yeah. And it's, it's, it's one of those things where I always kind of felt like in academic papers, um, there was, there's not really the incentive or the support to go out there and be like, let's, let's like do these induct user interviews. And, um, when I started Akita, I worked with a product designer very closely for a few months to, um, she project managed a user interviews where I was just spending weeks and weeks calling, you know, every security person calling a bunch of developers, you know, like anyone who had talked to me and doing these very controlled, very meticulous interviews of, you know, like tell me what happens in your life, starting from when you wake up, what's your workflow like, um, like, you know, digging into pain points they had.
Jean (00:43:28):
And I was just like, Holy crap. You know, for my whole career, I'd been, I had been saying these things around, where does this is who we're designing for? This is, you know, the pain points we're designing for this is when they fall down, but I just made it all up. So I like, this was deeply satisfying to me to finally, you know, uh, pay my dues and really understand what was going on.
Joey (00:43:48):
Yeah. I think, I think, you know, I did this, I did this in academia as well. And it's like, you kind of like, you're like, all right, well, I should make this like making it useful a lot of times it's not the point. Right. It's like, there's a great problem. I want to go after it. But like in the paper, I should say, who's maybe going to use this. I just say like, I should say things like why aren't people taking this like awesome tool that I built and you're like, why aren't they using it in industry? It's cause it's, cause they're not, you know, they're not trying hard enough, but like the more I put myself into exposure, it's like people are, people are working their butts off, out there. Yeah.
Jean (00:44:20):
Yeah. And it's just like, Oh, okay. That's their real problem. Not this one. Or that's how I realized no one can do any of the stuff that I want them to do. They're like 15 years off from doing this stuff I was working on before. Cause they need all this other stuff. And that was, um, that was a real revelation for me. And um, I guess I decided it was more satisfying for me to build the stuff they need in order to use this stuff.
Joey (00:44:42):
Yeah. And it seems like, it seems, you know, the, the 15 years off things hold holds true. Cause like I, I suspect you're finding this to some extent and what we see is like the things that feel most likely to see adoption, they're the things that people were doing 10 or 15 years ago.
Jean (00:44:55):
Yeah, yeah. No, exactly. And then like, people are like, well, you know, how to, how to PHP become a big thing or like, ah, like, you know, these languages that have no principles everyone's using them well, they're using them because they're solving problems they actually have. And if we want people to use our stuff, um, in, you know, widely from formal methods, from programming languages, we also need to solve problems that they actually have today. Not, you know, 10, 15 years from now, they will have the problem or 10, 15 years from now they'll, you know, snuck there. Hasn't say, Oh, I realize this is the problem we've been having for 15 years. Like, you know, they, they need to have the problem and know they have the problem. And that's actually been an extremely hard problem for us to solve. We're actively still working on it, obviously. Um, but, but you know, that that's been something that's been extremely rewarding and fun for me because after 10 plus years of just kind of making up what people's problems are, I'm getting to see what they are and solving them.
Joey (00:45:50):
I could take that whole, like couple of sentences and make it the jingle of this podcast. You know, we got it. Yeah. And I, and I think, you know, I think the doing the academic, like, you know, I I'm afraid this might come off as saying, you know, like doing the academic work is not valuable and you shouldn't make stuff up about how it might be useful. But again,
Jean (00:46:07):
I used to do that work too. Yeah. But you can't do both. I think
Joey (00:46:11):
Yeah. Benefiting from people 10 years ago, that made stuff up. And that, that made these, like people were thinking about fuzzing and it's like, okay, well fuzzing, like, why do we need to do that? You can verify, you know, you could, you could, you could do handwritten tests and now we're like, look, fuzzing is going to change the world.
Jean (00:46:26):
Yeah, absolutely. Yeah. I think there's a role for every kind of person. I think, you know, there, there needs to be people working on things 15 years out so that we don't run out of innovations 15 years from now. And then there needs to be people working on stuff 30 years out. So we don't run out of innovation, you know, the 15 year people have something to follow. But I think for me, I'm the, if the goal is a widespread adoption of something 15 years out is a really big bet because that funnel really narrows.
Joey (00:46:56):
Yeah, definitely. We're, we're, you know, we're lucky to have the body of work to go back on, basically that we have. And, and to have that, that great old research that is ready.
Jean (00:47:06):
And I think for a gala, the really cool part is I'm well, it it's like that fashion design analogy, which I can go over again now, but I'm one way I like to explain programming languages and formal methods research is it's, uh, the research languages and the research models, like your high school, your address, and, and also like the cock of star, all of that. That's like what you see in a runway show. So it's not intended for everybody to use. It's not intended for, um, you know, widespread adoption, but it's really pushing the boundaries of what's possible. And, you know, showing, showing the latest in art and science put together. And I think, um, what's really cool about Gail law is you guys are actually taking that runway stuff and like, you know, serving, serving like very cool, very important use cases with that.
Jean (00:47:58):
And so it's not like, you know, every developer at Facebook is verifying their whole thing end to end, but you know, at gala you can afford to take that and like verify the most critical pieces of Amazon infrastructure or something like that. And so, you know, it's, it's, it's, it's, it's, it's very, very cool to see that. And I think that it's very important to do that because like what you see what you see in the mainstream. So I think how I described it last time was your PHP and your Python. They were like the Hanes t-shirts right. Like they're like, it takes a while before the super avant garde stuff really trickles down to there. But I'm where I sit is like, let's, let's do some cool embellishments on your tee shirts that are affordable for everyone. Let's give you that an affordable jacket to wear with that. T-shirt. But if it wasn't for all the work that came before there can't be a trickle down. And how I spent my career earlier was I worked on, you know, super avant garde stuff. Yeah. Like if we could have refinement types on our things, this is, we can just like generate all of our access checks, checks who needs to write them anymore. But, you know, um, it's, it's just a completely different game. If you're trying to bring this technology to, to everybody,
Shpat (00:49:04):
I love this analogy because even for kind of formal methods people, it's a, it's a good kind of analogy to explain like, okay, some of this stuff may not be completely applicable to yeah.
Jean (00:49:14):
Yeah. Like no one like not, well, I mean like the, if you look out the window, no one is probably going to be wearing like, you know, complete face covering like head to toe gold or like the snakes all over their bodies or whatever they're doing. But, um, you know, so someone should be doing that. And, um, yeah, someone, um, responded to one way tweets with, um, have you guys watched the devil wears Prada? Okay. So, um, so there's a scene where Anna Wintour she's this like Vogue, Vogue editor and chief really big fashion person. She's um, talking to her new assistant, played by Anne Hathaway. And she's like the PR Anne Hathaway is just kind of giggling. She's like, everything looks the same to me, whatever. And Anna Wintour is like, Oh, you think this doesn't apply to you. And she takes her sweater and breaks down the shade of the blue and gives the entire, the entire history of like this designer first introduced this color, or this designer did this with it.
Jean (00:50:10):
And then, you know, like a bunch of other stuff happened. You probably found this in a bin somewhere and you don't care about it, but you know, this, even the sweater you're wearing has history and you know, every single construct and every single mainstream language, if we think about it came from somewhere, every single tool that people are using today came from somewhere. And I think there's, um, there's a lot of space in the programming languages research community. I think historically, if you were in the business of making the avant garde stuff, you didn't go all the way and design like the tee shirts. Um, well, that's actually not correct many fashion designers design t-shirts you don't design the tee shirts that people sell at target. Um, so the analogy I like is I want us to be the, uh, zag ms. Rocky for target, where, you know, you have like very good design at very affordable prices. Um, I think like there, there hasn't been so much of that, um, up until now.
Joey (00:51:03):
Yeah. And I think what's really great about that is like, we, you know, you talk about like, like a fashion designer with stuff on target shelves, right? Like how many people that are buying that, do you think actually even even cared, right? They're like, this is like, yeah, that's a, that's a cool shirt. It's a little longer in the front I'm kind of in the back. Right. And that works for them and they buy it.
Jean (00:51:20):
An interesting phenomenon is actually my fashion friends will like go and line up to get the target items or like their moms we'll go line up for them to get it for them. Um, cause I remember that like these lines started coming out when I was in college. And so like one of my friend's moms actually would like, wait in line for when target opened. Let me get that for her. But I mean, how cool is that, that someone who's used to buying like, you know, thousands of dollars per shirt is now waiting in line at target because this has been so democratized,
Joey (00:51:50):
But I mean, we're seeing it and we're seeing it in PL now, right? Like, like when, you know, 10, 10 years ago, if you told, like, if you told the developer to write a Lambda, they would look at you blankly.
Jean (00:52:01):
And half of my calls, people are like, do you support Liam does, it's a different kind of Lambda, but, but
Joey (00:52:07):
[inaudible], Oh, I mean, are you talking about,
Jean (00:52:10):
We're not related, it's just a different level.
Joey (00:52:12):
Yeah. But people, you know, people understand like a function without a name, as a Lambda. Right. Whereas like,
Jean (00:52:18):
And they understand how useful that is. It's such a clean abstraction model. People are now like sometimes. Um, so what we're doing with the block box testing, it's very, very analogous to fuzzing. One could call it fuzzing. Sometimes we explain it to people without saying the word fuzzing and they'll say, Oh, like a fuzzer. And it's awesome when people know that. And, and actually like for a lot of things, people say, Oh, how does this compare to static analysis or dynamic analysis or, um, there's, there's definitely a lot more literacy, um, uh, among all developers, uh, than there was 10 years ago. And that's super cool.
Joey (00:52:52):
Yeah. I think it's, I think it's really amazing and I, you know, I need to re remind myself, I guess another one is like, you know, like a C-sharp basically has, has pattern matching now, right?
Jean (00:53:02):
No, it's amazing. And Swift also, I'm also like, I don't know how many people have programmed enough sharp, but it has everything it's like the most beautiful language in the entire world and it all runs on, uh, on the CIL. So,
Joey (00:53:19):
Yeah. That's great. Um, cool. Let's let's let's do, let's see if we covered in the document. I didn't, I don't want you to have prepared any answers. Um, Oh yeah. So, you know, if I'm a, if I'm, if I'm about all this, I'm sorry. Um, if we, if we're taking breaks like that, um, let's, let's take a few seconds before starting to speak so we can cut. Oh, cool. Yep. I will, uh, I will take a deep breath first. So if I'm hearing about, if I'm hearing about formal methods and I'm hearing about the work that Akita might be doing now or in the future, and I kind of believe that that might apply to me, what, what should I do to, to help me understand if, if I need that kind of approach or to help build other evidence that I need, that, that kind of approach, if I, you know, say I'm a, I'm an engineer and my manager might not, might not believe in formal methods, but I kind of want to show how formal methods can help.
Jean (00:54:19):
Absolutely. So I think a lot of that, that's a great question, first of all. Um, but yeah, I think a lot of that, um, is on us. Um, so, so right now, like I said, we're in stealth, but, um, hopefully the value proposition that we, uh, believe, uh, for, for these developers is also the value proposition that their managers believe. Um, so at a very high level, um, who I would like to be talking to us is developers that have, um, have software that talks to, um, that gets talked to you or talks to other things through APIs, um, developers that want to know what's going on with the data and their software, either for security or privacy reasons, or just for general software quality reasons, because, um, most software is about moving data from one place to another in, um, in, in web web applications.
Jean (00:55:12):
Um, and, um, and there's, there's a lot there, but, um, but yeah, so I think that, um, we have some pretty strong value props around. We can, um, we can help you with audit. We can help you with, um, data governance, uh, kinds of things. Um, and we're, we're happy to see a much more, um, in, in like a one on one setting then than on our website or, or on a podcast. But, um, I would say of developers think that, um, they want, um, I wouldn't like we don't call it formal methods in any way. Like these are very, very, very, uh, digestible tools. Um, it's, it's been a fine line actually walking, walking the line between like, these are actually power tools, um, that, you know, are influenced by words that you probably don't want to say to a manager versus these are very similar to like the CIA tools, you know, and love. Um, but I would say developers should talk to us. Um, I'm happy that to tell them more, um, you know, offline, and then we can have a conversation around like, do they, do they have the problems that our value props help serve?
Joey (00:56:15):
Yeah. I'm really interested in this question that you just kind of highlighted about, like when we're marketing our, you know, we, we kind of know it's formal methods, right? We, at the core what the science is, why this is a good thing to do. Um, yeah. Like, is it better to like, try to make, you know, cyber became a word like big C cyber became a word awhile back. Right. And people were like, I need to get some, some cyber. Yeah. Um, do you think, do you think big F formal is, is a, is a thing or is it, or is that the wrong way to go about?
Jean (00:56:44):
I think formal is not a thing yet. I'm one stereotype. I had to fight pretty hard when I started the company was, um, I think PL academics are not very cool industry. Um, I mean, I think, I think they think we're good for like, tell me about like your homo topi type theory and stuff, but the minute I was like, Hey, so I can build you some tools that you'll use. They're like, Ooh. Cause they, you know, like what have you been associated with PL academia, like kind of terrible developer experience. You probably need like a few metals and math Olympiads to understand the output of the tool, um, and all this stuff. And so like, I think it's been great for, you know, people are happy to commission some PL academics and prove something for them, but if we're starting to put ourselves behind the tools that they're going to use, I think there's a lot of skepticism.
Jean (00:57:35):
And so what we've been trying to do is work on extremely easy product design. So, um, my, uh, third hire was a product manager who came from Twilio, which is like the most developer friendly company ever. And so I think there's been, there was a definitely a very long period where he, um, someone had, he had worked with, had previously worked with academics and told him like, Oh no, it's like terrible man. So like, I try to talk to them and I can't understand what they're saying. They don't come to things like they have no agenda and they're just like going like this all the time. And so there was definitely a period of time where I'd be like, no, like I think one time we had a meeting where he was like, so, so you want to do things right? Like we want to ship code. And I said, yeah, we absolutely want to ship code, but there's, um, I think there's definitely some, uh, major skepticism, um, to academics, you know, shipping tools that people use at large. Um, I do not think it is done very often, but, uh, that's what, that's what we're trying to do here.
Joey (00:58:39):
Yeah. We used to encounter that a lot and that's, so this, this divide, right. I think is where we're, where that problem is mostly lives.
Jean (00:58:50):
Yeah. It's just, it's very, it's very two very different cultures. Um, and I think there's a lot of things, um, that are amazing about academic culture. I think, you know, the, the culture around inquiry, the culture around creativity, it's all great. But when it comes to programming tools, there's kind of an anti user experience culture that, um, as programming language designers, it's very interesting to me, um, where it's like, what, you know, like they should definitely be able to like write all these like hundred line proof terms by hand. Uh, you know, what do you mean when she gets some HCI people to take a look at this? Um, but you know, when I was, um, at my first pothole that I ever attended in 2009, Greg Morris, who's one of the big names and, you know, uh, provable approvable guarantee use and software verification, he had said, you know, I think programming languages, people should be collaborating a lot more with, um, human computer interaction people because a lot of the problems in programming languages are actually how we interface with people. And that was something I thought about for years and how I feel like I'm finally embracing that is, um, just, you know, doing a ton of user research and making developer experience a first class, uh, value in our company.
Joey (01:00:03):
So, you know, on that, but on the other, on the other hand of this, right, we have, like, if we look at sort of what's happened recently with machine learning or blockchain or any of the other things that kind of, you know, have had moments recently, um, the companies have been, you know, banging on people's doors, like formal methods, people, to some extent out of blockchain have like been getting cold calls, saying, come help with my blockchain. Can we see that for formal methods instead of, for, instead of for blockchain?
Jean (01:00:30):
Yeah. Maybe blockchain is just our one win. Um, yeah. The best and brightest minds of our generation, all doing blockchain verification. Um, um, I mean, I hope so. Um, I don't know, man, I think maybe we need a sexier name, Lind formal methods. It seems like very elite. I think, I think there's a lot of it is a marketing problem. I think, um, you know, programming languages, like has always like the people come from philosophy and logic, which like, you know, aren't the most, like we need to reach the masses kind of kind of people. Um, so I think, I think there are some, um, some, some traditions against kind of, um, meeting, meeting the people where they are. Um, but I think, I think software tooling is, is having like, is having a big moment right now. I think that, you know, um, Microsoft, you know, they bought get hub.
Jean (01:01:24):
They're like the developer tools company right now. And they kind of always were during my whole PhD too. I mean, I'm, Asara was like the place to be. Um, I was obsessed with like pretty much every software demo I saw during my internships there. Um, but you know, like I think for awhile it was, it was kind of like the research thing, but I think that stuff has really been trickling into, into Microsoft, um, the whole as a whole, you know, vs code as a thing. So I think, I think developer developer tooling is becoming a big thing. I think there's, um, there's also more activity around testing. Um, maybe it's just my filter bubble, but fuzzing is very cool now. Um, and I, I think, I think especially in a time where people want something shiny, um, automated testing just feels like eating candy or flying or, you know, something like that.
Jean (01:02:14):
Um, but, but I think that, um, I think that software tooling will have a, um, and then I think once people realize that software tooling has really not entered the automation era, I hope that people will start, uh, looking to the better things. But, but I think it's, it's one of those things where there hasn't been the breakthrough tools yet to really show people what's out there. Um, so I looked this up online yesterday, but do you know the first car? It was like way slower than the horse, like the fastest horse. And it's like, it was actually also slower than probably like a medium horse too. But I think in terms of where we are with, with formal methods, like in practice, um, I think people who really know what they're doing can use things like cock is about, um, F star address Haskell there's.
Jean (01:03:08):
I have a lot of debates with people about like, they're like high school, so mainstream, not a research language. And I'm like, I love high school. I have used high school personally at Facebook, but you know, it is a, I would not call it a mainstream language. It's pretty obscure. You like have one of your constructs named after monads like, that's, that's not like accessible. Um, but, um, but yeah, I think, um, I think, you know, like this tooling is making its way into the mainstream. I think it's becoming, it's starting as like a niche thing where people like self teach themselves depending types and things. Now, um, there's more textbooks out there to do that. I think, you know, slowly or quickly this is going to spread. I don't know how yet. Um, I hope to be part of that and, uh, I think it will happen.
Shpat (01:03:54):
It sounds like you have a pretty good idea though. I mean, there's idea of what are the benefits? What does, what, what does it get you versus?
Jean (01:04:02):
Yeah, absolutely. I think you have to start with giving the people what they want. This is my philosophy and all the things. So I'm an unrelated, but related thing is when I was a graduate student, I, um, I cofounded graduate women at MIT on MIT campus. And before that, like feminism was a dirty word, but nobody even knew what feminism meant. So like, it's kind of actually very similar to formal methods. No one knows what it means, but they don't like it somehow. There's like something wrong with it. Um, you know, that's kind of an exaggeration, but you know, that's, that's kind of like all the spaces I'm in right before, well, methods, compliance, security, privacy, like no one really knows what it means, but they just don't like, it it's very much the opposite of stuff where they're like, I don't know what that means, but it's cool.
Jean (01:04:43):
Right. But what we, um, what we did was, um, I thought about, you know, what do people want? They want to advance their careers. They want there to be like more women in their classes cause they don't want to be the only guys. And like, you know, there's a lot of other stuff going on. And so I think we, we did some stuff that was pretty innovative for like women's groups at the time. Um, we had like non women focused programming, actually. Like we had stuff that was just like, this is how you do online branding. This is how you do assertive negotiate negotiation. This is how you do communication. And this is how you do like things that are just good for you in life. Um, we opened up all the events to men. Um, I was like, we should not keep them to women only like everyone should come, but there should always be a component of like, this is like helpful for women.
Jean (01:05:24):
And then, um, we were just very effective. Like we just like got shit done. Like we, we were like one of the best run organizations on campus. Like I'm not like, so I guess on tooting our own home. But like every year we won all these awards for like best org on campus. Like we did. Um, we did workshops for a lot of the other orgs on branding and stuff. We had like, you know, tens of Ks and budget, which is also very high for a graduate student random group. Um, but I think it was through just like getting shit done and also kind of breaking out of, of the, the stereotypes that we were able to, um, to, to really build, um, build a new brand around words that were previously considered not cool or dirty words, even. So I, I mean, I think that for, I don't know, I guess blockchain just started out being cool and formal methods just kind of secretly got its way into there, but you know, I think there's, there's, there's ways to fix an image problem. It's it's a communication problem. It's a, it's a marketing problem. It's a branding problem in some way. Um, and, and there, there are ways to fix it.
Joey (01:06:22):
Yeah. We just need to go, go call it a business casual methods.
Jean (01:06:28):
There's just enough things that, that people like that they find useful. And you're like, Hey, by the way, this was formal methods. The whole time, like what we did with feminism was actually three years in, we had a panel that was a feminism panel and what we call it, it was, I'm not a feminist, but, and then our, our ad campaign was actually, um, it was a postering campaign to really raise awareness about feminism, but no one knew, but the ad campaign was like, the title was, I'm not a feminist spot. And then we had speech bubbles that were like, I believe men and women should have equal pay or I wish there were more women in my department or things that it was just like, people should believe to be true if they like were thinking, and this was, this was nuts. Cause all these people are like, wow, I didn't realize I was a feminist. And so this was three years in after people had been like going to our programming, we had established ourselves as a presence on campus. And so I think it's one of those things where like for all month it's just has to take over everything. And then we're like, Hey, you know, you might think that you hate this stuff, but actually even using it the whole time and it's very helpful to you. Um, and then that's how we win.
Joey (01:07:29):
It doesn't matter what it's called. Right?
Jean (01:07:31):
Yeah. Like you just have to get in there
Joey (01:07:34):
A side question. Have you ever written about that experience?
Jean (01:07:37):
Um, I have a medium post. I think the medium post was like, it's called give the people what they want. Like you always just have to give people exactly what they want as fast as they want it. And then like you can do anything you want.
Joey (01:07:48):
Right. Yeah. Sounds like there's a lot of learning from
Jean (01:07:52):
Like today. I was talking to someone like, how do you talk to journalists? And like, Oh no, just like talk to them as soon as they want to, whenever they want to and tell them whatever they want to hear. And then they were like, I think this is just how you want it. Everything. Um, well I think for tools, you actually have to produce the results, but,
Joey (01:08:08):
But one of the things I had to fight against, you know, pretty hard that I think, I don't know if I learned it in academia or I thought it coming into academia was that like, it's important to
Shpat (01:08:16):
Be modest and to not want to sell your stuff and like it, at some point I had this mindset. Right. And I've totally gone one 80 on it. It's like,
Jean (01:08:23):
Yeah, I don't even think that's an academic thing. I think one reason, like, I feel like having a company I like more is I feel like in academia, there's a, there's actually this whole game and I'm not dissing the game. It's just what the game is, is you have to like spin your work a certain way. Right. And then you have to be like, this is who's going to use it. And this is why they matter. Um, whereas like, I don't know. I feel like if you're building stuff and people use it, you're just like 1 million people use my thing today. And so, I don't know. I think there's like many ways to many ways to sell something. And if you actually have the metrics to back something up, it's easier.
Shpat (01:09:00):
I see. So you like the, you liked that the metrics that you're measuring right now, you feel like are, are much more direct and much more, more meaningful to what you're trying to get done.
Jean (01:09:12):
I think so. Cause I, I, like, I always felt like for the papers I was writing, at least, especially because I was interested in these kinds of impacts, I would have to make all this stuff up. Like there are this many people doing this kind of thing. And like, this is like how this will impact them. But like there's, there's, it was not part of the incentive structure to prove any of that. Right. Um, whereas now like, you know, like in order for us to like raise our next round of funding, we have very specific metrics that I feel like are tied to like our thing being actually useful.
Shpat (01:09:37):
Yeah. That's great. Yeah. I think that the, the lowest bar is there just to show this stuff in action, right. Just to talk about that stuff. So for us to resemble some of the, some of the work we've done with Amazon web services, I mean, just, just talking about that people and then they started digging into it and you see all these big companies kind of applying some of this stuff.
Jean (01:10:00):
No, I think I got a lot. You guys are amazingly positioned to contribute to the formal methods branding problem, because like, you guys are actually doing tons of cool stuff in action all the time, but I think, you know, outside of, um, outside of the people who are already following this stuff, I don't know how many people know about this. Yeah. But like I always had so much on V for Galloway people. Um,
Shpat (01:10:22):
Yeah. I definitely wasn't milking for yeah,
Jean (01:10:24):
No, but it's it's, you guys are like, you guys are doing such cool stuff, but you know, if I, if I talk to, you know, a friend who's a software developer and I say gal law, they might be like, what? And then, you know, then I'll have to say, do you know that you can even do this with your programs? And they're like, what? And then, you know, it just, it's so many steps, but I think the literacy is getting better.
Shpat (01:10:44):
I agree. I can't think of a better place that kind of stopped. It sounds like we could talk about this stuff for, for the rest of the day, but I know that this was, this was an amazing conversation and I know you're very busy. Um, and I just want to thank you for spending this time with us. It was very enlightening. I enjoyed this conversation a lot and I really look forward to seeing to seeing where you, where you take Akita. I'm sure there's great things over the horizon. Thank you very, very much for joining us.
Jean (01:11:18):
Yeah. Thank you guys. This was super fun.
Shpat (01:11:20):
Awesome. Well, this was an episode of building better systems and, uh, we, we will see you in the next one.