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 two of a two-part episode. Please make sure to check out part one.
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
Shpat (00:00):
This is part two of a two-part episode, find the first part, linked in the description.
New Speaker (00:07):
The designing, manufactory, installing and maintaining the high-speed electronic computer, the largest
and most complex computers ever built.
Joey (00:27):
So I was going to go back to something I heard you say earlier, which it sounded like a bit of a personal philosophy that I, that I wanted to dig into as you, you kind of said, uh, get shit done. Is that like a thing you do? Like sometimes, you know, let's see, this is, this is going a bit into, to work style and out of formal methods, but like you've started a company, right? Like, did you just go do that? Like what, how you just woke up one day and said, I'm going to, I'm going to do it?
Jean (00:51):
Well, it was, um, a series of events that led to the company starting, but people tell me everything, uh, is caused by a series of events. But, uh, essentially what happened was, um, I commit to things very quickly, um, after thinking about them very fast and then I follow through. And so that's kinda how it happened. So, um, it was, uh, early 2018. 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. How did you pick privacy?
Jean (01:38):
Is Facebook going to matter in 10 years? Isn't privacy just going away. And so, um, I, I had kind of, my bet was in 10 years, people are going to 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, does that even matter? And here 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 is 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. And they said, well, you know, we really need to know where our data goes in our software now.
Jean (02:21):
And I was just like, what is going on? And so this was such a, a different audience than I had ever existed before that I felt it was very important to take note. So that was kind of the proximal, uh, trigger for all this. But I think for a very long time, I sort of concluded that, um, for some of the impact I wanted to make 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 spent a lot of time looking at other, other tech transfer stories. 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. And so I conclude at some point that, you know, if I started a company, it would have to be very much around the software tools, programming, guarantees, things like that.
Jean (03:07):
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 we got a VC firm to give us some money and commit to giving us office space where we sourced teams in the cybersecurity space. Initially it was cybersecurity research like PhD kind of people. And then they would give, um, initial funding and office space 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 tied to regulatory shift because nobody cares about security otherwise. And 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.
Jean (03:54):
I should really look into this. And so at that point, I was two years into my tenure track position at Carnegie Mellon. It's not really the time you just, you know, take a sabbatical, like you don't get a sabbatical two years in. You also don't have a lot of momentum. So I had just raised like a couple million dollars where I was a 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. Um, because I recognized at that point, if you take a leave, you're pretty much winding down your entire momentum. 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.
Jean (04:34):
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 were doing with their data, what their software situation is, and really assessing the situation. 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. So 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. And, um, then when you file for leave, you, you know, you have to switch over your, your teaching requirements of the fall and all that stuff. By the time you file for leave, you you're pretty much committed to taking, 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.
Jean (05:15):
So I should probably give up my apartment. 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, the company, I had nothing left. I had no group, I had no house, I had no furniture. And so, um, in some ways it was the easiest decision I've ever made, because I think the worst kind of decision is one you make too quickly and you regret it. Or one, that's not really like a firm decision where you're like, all right, 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 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, he was 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. So I was forced into a series of decisions that made the ultimate decision very easy and in some way,
Joey (06:16):
But it's, it sounds like it was a path you put yourself on a, you know, 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 this situation where it's like, if we don't get this episode done, we're gonna, we're gonna let Jean down. We're gonna let, we're gonna let all these other people we're interviewing down. So
Jean (06:33):
Yeah. Yeah. I, yeah. It's, it's definitely true. It's it's yeah. It's one of those things where you're like, all right, I'm going to do this next thing because I want to, and then you were like, yup. There's no, there's no going back now. 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 (06:48):
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, we know we know what the end game is here. Right? One of the limitations I see in, you know, the, that I'm a bit envious of you, although, you know, you've earned this through hard work is basically like exposing yourself to lots of problems. Basically. It's, it's really hard to reach out to like th this, uh, 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 hard. Like it's hard to t. So many of these conversations, it's hard to ask people for things. And then you have to wrap your head around like all of these different problems that people come at it from different ways. But like in the end, I, it seems like it's really crystallized your idea of what, of what you need to do.
Jean (07:34):
Yeah. Well, I think we're still testing and iterating, but I think, yeah, the product work that we've been doing has really been helpful. And 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 in the, you know, two sentences of your, the impact of this and your conclusion. But I think that work to me is really satisfying to be able to actually justify this as who's going to use it. And I think you guys at Galois 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 (08:19):
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 I'm dollar Kickstarter. Yeah. And it's, it's one of those things where I always kind of felt like in academic papers, there's not really the incentive or the support to go out there and be like, let's like do these in- depth 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, you know, digging into pain points they had.
Jean (09:19):
And I was just like, Holy crap. You know, for my whole career, I had been saying these things around, where did 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 (09:39):
I think, I think, you know, I, 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. 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 gonna use this. I should say, like, I should say things like why aren't people taking this like awesome tool? Like why aren't they using it and industry it's cause it's, cause they're not, you know, they're not trying, but like the more I put myself into exposure, it's like people are, people are working their butts off.
Jean (10:08):
Yeah. 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. They're like 15 years off from doing this stuff I was working on before, because they need all this other stuff 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 (10:27):
Yeah. And it seems like, it seems, you know, the, the 15 years off things hold holds true. Cause like 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 (10:39):
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 their heads and say, Oh, I realize this is a 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, uh, 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 (11:32):
I can take that whole, like couple of sentences and make it the jingle of this podcast. No, 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 (11:49):
Yeah. No someone needs to do that work too. Yeah. But you can't do both. I think what I realize. Yeah.
We're benefiting
Joey (11:54):
From people 10 years ago that that made stuff up. And that, that made these like, like people were thinking about fuzzing and it's like, okay, well buzzing. Like, why do we need to do that? You could do handwritten tests. And now we're like, look, fuzzing is going to change the world.
Jean (12:08):
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 innovations, 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 (12:33):
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 great old research that is right.
Jean (12:42):
Yeah. And, and I think for Galois, the really cool part is I'm well, it it's like that fashion design analogy, which I can go over again now. But, um, one way I like to explain programming languages and formal methods research is it's the research languages and the research models, like your Haskell, your address, and also like the Coq, Fstar, 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 what's really cool about Galois is you guys are actually taking that runway stuff and like, you know, serving like very cool, very important use cases with that. 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.
Jean (13:42):
And so, you know, it's, it's, it's very cool to see that. And I think that it's very important to do that because what you see in the mainstream. So I think how I described it last time was your PHP and your Python. They're like the Hanes t-shirts right. Like it takes a while before the super, um, avant-garde stuff really trickles down to there. But, um, where I sit as like, well, let's do some cool embellishments on your t-shirts that are affordable for everyone. Let's give you that an affordable jacket. Where would 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 is we can just like generate all of our access checks, checks who needs to write them anymore. But you know, it's just a completely different game. If you're trying to bring this technology to everybody,
Joey (14:29):
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 the everyday program.
Jean (14:40):
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, 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. Well, so, um, so there's a scene where Anna Wintour, she's this like Vogue Vogue editor in chief, really big fashion person. She's talking to her new assistant, played by Anne Hathaway and Hathaway is just kind of giggling. She's like, everything looks the same to me, whatever. Um, 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 (15:31):
And then, you know, like a bunch of other stuff happened. You probably found this at 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, 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, um, design like the t-shirts, but what that's actually not correct. Many fashion designers designed t-shirts you don't design the t-shirts that people sell at target. So the analogy I like is I want us to be the Issaquah ms. Rocky for target, or, you know, you have like very good design, very affordable prices. Um, I think like there, there hasn't been so much of that up until now.
Joey (16:20):
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. And they're like, yeah, that's a, that's a cool shirt. It's a little longer in the front. I'm kind of into that. Right. And that works for them. And they buy, yeah.
Jean (16:37):
An interesting phenomenon is actually my fashion friends will like go in 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 one target open, like 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 (17:06):
But I mean, and we're seeing it and we're seeing it in PL now, right? Like when, you know, 10, 10 years
ago, if you told, like, if you told a developer to write a Lambda, they would look at you blankly and now Jean (17:16):
Yeah, yeah. Now like half of my calls people are like, do you support? Does it's a different kind of Lambda, but, but um, yeah, they, they are related. It's just a different level of abstraction
Joey (17:28):
People, you know, people understand like a function without a name, as a Lambda. Right.
Jean (17:32):
Yeah. It's awesome. And they understand how useful that is. It's such a clean abstraction model. Um, people are now like sometimes, um, so what, what we're doing with the black box testing, it's um, very, very analogous to fuzzing. One could call it buzzing. Sometimes we explain it to people without seeing the word buzzing, they'll say, Oh, like a buzzer. And it's awesome when people know that. And then 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, uh, among all developers, uh, than there was 10 years ago. And
Joey (18:05):
Yeah, I think it's, I think it's really amazing. And I, you know, I need to remind myself, I guess another,
another one is like, you know, like a C-sharp basically has, has pattern matching now. Right?
Jean (18:14):
Yeah. I know. It's, it's amazing. And Swift also, um, also like, I don't know how many people program enough sharp, but it has everything it's like the most beautiful language in the entire world and it all runs on a, on a CIL.
Joey (18:29):
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 should I do to, to help me understand if, if I need that kind of approach or to help build up the 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 believe in formal methods, but I kind of want to show how formal methods can help.
Jean (18:55):
Yeah, absolutely. So I think a lot of that, that's a great question first of all, but yeah, I think a lot of that, um, is on us. So, so right now, like I said, we're in stealth, but, um, hopefully the value proposition that we believe 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 have software that talks to, that gets talked to, or talks to other things through APIs, um, developers that want to know what's going on, uh, 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 applications. 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.
Jean (19:49):
We can help you with audit. We can help you with data governance, uh, kinds of things. And we're, we're happy to say much more, um, in like a one-on-one setting then than on our website or, or on a
podcast. But, um, I would say have developers think that I wouldn't like we don't call it formal methods in any way. Like these are very, very, very, uh, digestible tools. It's been a fine line, actually walking, walking the line between like, these are actually power tools 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, you know, offline, and then we can have a conversation around like, do they have the problems that our value props help serve?
Joey (20:36):
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, we know at the core what the science is, why this is a 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 cyber. Yeah. Yeah. Um, 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 (21:05):
I think formal is not a thing yet. Um, one stereotype I had to fight pretty hard when I started the company was, um, I think PL academics are not very cool in history. Um, I mean, I think, I think they think we're good for like, tell me about like your home 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, cause they, you know, like what do people associate 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, it's been great for, you know, people are happy to commission some peel, academics 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 (21:54):
And so what we've been trying to do is work on extremely easy product design. So, um, my 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 a, 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 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 (22:55):
Yeah. We used to encounter that a lot in that. So this, this divide right. I think is where we're, where that
problem is mostly lives. Jean (23:03):
Yeah. It's just, it's very, it's 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 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, you know, what do you mean? We should get some HCI people to take a look at this. But you know, when I was, um, at my first pop hole that I ever attended in 2009, Greg Morrison, who's one of the big names and, you know, provable approvable guarantee use. And in 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 (24:13):
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, 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 like, come help me with my blockchain. It's nuts. Can we see that for formal methods instead of four steps for blockchain?
Jean (24:40):
Yeah. Maybe blockchain is just our one win. Um, yeah. The best and brightest minds of our generation, all doing blockchain verification. 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, 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, some, some traditions against kind of, um, meeting, meeting the people where they are. But I think, I think software tooling is, is having like, is having a big moment right now. I think that, you know, Microsoft, you know, they bought get hub.
Jean (25:29):
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, I was obsessed with like pretty much every software demo I saw during my internships there. 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 as a whole, you know, vs code is a thing. So I think, I think developer developer tooling is becoming a big thing. I think there's also more activity around testing. Um, maybe it's just my filter bubble, but fuzzing is very cool now. Um, and 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. But, but I think that software tooling will have a moment.
Jean (26:16):
And then I think once people realize that software tooling has really not entered the automation era, I hope that people will start looking to the better things. But, but I think 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, 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, I think people who really know what they're doing can use things like Coq, Isabelle Idris, Haskell there's. I have a lot of debates with people about like, they're like high school. So mainstream, not a research language.
Jean (27:04):
And I'm like, I love Haskell. I have used Haskell personally at Facebook, but you know, it is, uh, 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 yeah, I think, you know, like this tooling is, is making its way into the mainstream. I think it's becoming it starting as like a niche thing where people like self-teach themselves dependent 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. I, I hope to be part of that and uh, I think it will happen.
Shpat (27:42):
It sounds like you have a pretty good idea though. I mean, this idea of what are the benefits, what, what
does it get you versus this is what it is.
Jean (27:49):
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 co- founded 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, like that's, that's kind of like all the spaces I'm in, right? Formal 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 (28:29):
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 because 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 negotiation 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. 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 (29:09):
And then, um, we were just very effective. Like we just like got shits on, like, we were like one of the best run organizations on campus. Like I'm not like, so I guess I'm tooting our own home. But like every year we won all these awards for like best Oregon 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 graduate student random group. Um, but I think it was through just like getting shit done and also kind of breaking out of the stereotypes that we were able to, um, to, to really build a new brand around words that were previously considered not cool or dirty words, even. So, 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, 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 that.
Joey (30:04):
I agree. Yeah. We just need to go, go call it a business casual methods. Right.
Jean (30:11):
I think if 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 of 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 were 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 a whole 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. And then that's how we win.
Joey (31:10):
I love that. Then it doesn't matter what it's called. Right.
Jean (31:13):
Yeah. Like you just have to get in there. That's a side
Joey (31:16):
Question. Have you ever written about
Jean (31:18):
That experience? I have a medium post. I think the medium post is 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 (31:29):
So it sounds like there's a lot of learning from what you,
Jean (31:32):
Yeah. Like today I was talking to someone like, how do you talk to journalists? And like, I don't know, 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. Well, I think for tools, you actually have to produce the results. But,
Joey (31:48):
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 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 (32:03):
Yeah. I don't think I, 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 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, I don't know. I think there's like many ways to sell something. And if you actually have the metrics to back something up, it's easier.
Joey (32:37):
I see. So you like, do you like that the metrics that
Shpat (32:40):
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 to?
Jean (32:47):
Yeah, 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 impact, I'd 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, it was not part of the incentive structure to prevent you 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 (33:13):
Yeah. And I think that the, the lowest bar is there just to show the 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 like, wait, wait, what? It's incredible. Yeah. And then they started digging into it and you see all these big companies kind of applying some of this stuff quite directly to them.
Jean (33:34):
Yeah. 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, I always had so much empathy for Galois people.
Shpat (33:56):
Um, because I definitely wasn't milking.
Jean (33:58):
Yeah. I know you guys are like, you guys are doing such cool stuff, but you know, if I, if I talked 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 were like, what? And then, you know, it just, it's so many steps, but I think the literacy is getting better
Shpat (34:18):
Great. I can't think of a better place to stop. It sounds like we could talk about this stuff for the rest of the day. Um, but I know that I love talking about this stuff and this was, this was an amazing conversation. And I know you're, you're very busy. Um, and, and I just want to thank you for spending this time with us. It was very enlightening. I enjoyed this conversation a lot. 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
Jean (34:49):
Yeah, Thank you guys. This was super fun.
Shpat (34:51):
Awesome. Well, this was an episode of building better systems and we will see you in the next one.