00:00:00.000 --> 00:00:00.111 [TEASER] [MUSIC PLAYS UNDER DIALOGUE] 00:00:00.111 --> 00:00:05.520 SHAN LU: I remember, you know, those older  days myself, right. That is really, like,   00:00:05.520 --> 00:00:09.720 I have this struggle that I feel like I  can do better. I feel like I have ideas   00:00:09.720 --> 00:00:16.240 to contribute. But just for whatever reason,  right, it took me forever to learn something   00:00:16.240 --> 00:00:22.040 which I feel like it's a very mechanical  thing, but it just takes me forever to learn,   00:00:22.040 --> 00:00:26.480 right. And then now actually, I see  this hope, right, with AI. You know,   00:00:26.480 --> 00:00:33.880 a lot of mechanical things that can actually now  be done in a much more automated way, you know,   00:00:33.880 --> 00:00:40.200 by AI, right. So then now truly, you know,  my daughter, many girls, many kids out there,   00:00:40.200 --> 00:00:46.480 right, whatever, you know, they are good  at, their creativity, it'll be much easier,   00:00:46.480 --> 00:00:53.524 right, for them to contribute their creativity to  whatever discipline they are passionate about. 00:00:53.524 --> 00:00:55.440 [TEASER ENDS] GRETCHEN HUIZINGA: You’re listening to Ideas, 00:00:55.440 --> 00:01:00.040 a Microsoft Research Podcast that dives  deep into the world of technology research   00:01:00.040 --> 00:01:13.240 and the profound questions behind the code. I'm  Gretchen Huizinga. In this series, we'll explore   00:01:13.240 --> 00:01:21.183 the technologies that are shaping our future  and the big ideas that propel them forward. 00:01:21.183 --> 00:01:21.200 [MUSIC FADES] 00:01:21.200 --> 00:01:25.160 Today I'm talking to Shan Lu, a  senior principal research manager at   00:01:25.160 --> 00:01:29.920 Microsoft Research and a computer science  professor at the University of Chicago.   00:01:30.720 --> 00:01:34.560 Part of the Systems Research Group, Shan  and her colleagues are working to make our   00:01:34.560 --> 00:01:41.560 computer systems, and I quote, “secure, scalable,  fault tolerant, manageable, fast, and efficient.”   00:01:41.560 --> 00:01:48.200 That's no small order, so I'm excited to explore  the big ideas behind Shan's influential research   00:01:48.200 --> 00:01:54.071 and find out more about her reputation as a bug  bounty hunter. Shan Lu, welcome to Ideas! 00:01:54.071 --> 00:01:54.880 SHAN LU: Thank you. 00:01:54.880 --> 00:02:00.080 HUIZINGA: So I like to start these episodes  with what I've been calling the “research origin   00:02:00.080 --> 00:02:05.640 story,” and you have a unique, almost  counterintuitive, story about what got   00:02:05.640 --> 00:02:10.700 you started in the field of systems research.  Would you share that story with our listeners? 00:02:10.700 --> 00:02:18.040 LU: Sure, sure. Yeah. I grew up fascinating  that I will become mathematician. I think I   00:02:18.040 --> 00:02:26.720 was good at math, and at some point, actually,  until, I think, I entered college, I was still,   00:02:26.720 --> 00:02:29.840 you know, thinking about, should I do  math? Should I do computer science?   00:02:31.200 --> 00:02:35.520 For whatever reason, I think someone told me,  you know, doing computer science will help you;   00:02:35.520 --> 00:02:43.480 it's easier to get a job. And I reluctantly pick  up computer science major. And then there was a   00:02:43.480 --> 00:02:52.040 few years in my college, I had a really difficult  time for programming. And I also remember that   00:02:52.040 --> 00:02:58.560 there was, like, I spent a lot of time learning  one language—we started with Pascal—and I feel   00:02:58.560 --> 00:03:06.920 like I finally know what to do and then there's  yet another language, C, and another class, Java.   00:03:06.920 --> 00:03:15.080 And I remember, like, the teacher will ask us to  do a programming project, and there are times I   00:03:15.080 --> 00:03:23.320 don't even, I just don't know how to get started.  And I remember, at that time, in my class, I think   00:03:23.320 --> 00:03:30.200 there were … we only had like four girls taking  this class that requires programming in Java,   00:03:30.200 --> 00:03:38.200 and none of us have learned Java before. And  when we ask our classmates, when we ask the boys,   00:03:38.200 --> 00:03:47.360 they just naturally know what to do. It was  really, really humiliating. Embarrassing. I   00:03:47.360 --> 00:03:55.400 had the feeling that, I felt like I'm just  not born to be a programmer. And then,   00:03:55.400 --> 00:04:00.080 I came to graduate school. I was thinking  about, you know, what kind of research   00:04:00.080 --> 00:04:05.880 direction I should do. And I was thinking that,  oh, maybe I should do theory research, like,   00:04:05.880 --> 00:04:11.440 you know, complexity theory or something.  You know, after a lot of back and forth,   00:04:11.440 --> 00:04:18.960 I met my eventual adviser. She was a great, great  mentor to me, and she told me that, hey, Shan,   00:04:18.960 --> 00:04:26.360 you know, my group is doing research about finding  bugs in software. And she said her group is doing   00:04:26.360 --> 00:04:34.000 system research, and she said a lot of current  team members are all great programmers, and as   00:04:34.000 --> 00:04:40.880 a result, they are not really well-motivated  [LAUGHS] by finding bugs in software! 00:04:40.880 --> 00:04:42.360 HUIZINGA: Interesting. 00:04:42.360 --> 00:04:46.120 LU: And then she said, you are  really motivated, right, by,   00:04:46.120 --> 00:04:51.680 you know, getting help to developers, to help  developers finding bugs in their software,   00:04:51.680 --> 00:04:56.080 so maybe that's the research project  for you. So that's how I got started. 00:04:56.080 --> 00:04:59.640 HUIZINGA: Well, let's go a  little bit further on this mentor   00:05:00.160 --> 00:05:05.080 and mentors in general. As Dr. Seuss  might say, every “what” has a “who.”   00:05:05.080 --> 00:05:10.720 So by that I mean an inspirational person or  people behind every successful researcher's   00:05:10.720 --> 00:05:16.840 career. And most often, they're kind of  big names and meaningful relationships,   00:05:16.840 --> 00:05:22.760 but you have another unique story on who has  influenced you in your career, so why don't   00:05:22.760 --> 00:05:28.560 you tell us about the spectrum of people who've  been influential in your life and your career? 00:05:28.560 --> 00:05:31.680 LU: Mm-hmm. Yeah, I mean, I  think I mentioned my adviser,   00:05:31.680 --> 00:05:36.560 and she's just so supportive. And I  remember, when I started doing research,   00:05:36.560 --> 00:05:41.240 I just felt like I seemed to be so far  behind everyone else. You know, I felt like,   00:05:41.240 --> 00:05:46.880 how come everybody else knows how to ask, you  know, insightful questions? And they, like,   00:05:46.880 --> 00:05:52.600 they know how to program really fast, bug free.  And my adviser really encouraged me, saying,   00:05:52.600 --> 00:05:57.360 you know, there are background knowledge that  you can pick up; you just need to be patient.   00:05:57.360 --> 00:06:02.440 But then there are also, like, you know how to  do research, you know how to think about things,   00:06:02.440 --> 00:06:06.769 problem solving. And she encouraged me  saying, Shan, you're good at that! 00:06:06.769 --> 00:06:06.796 HUIZINGA: Interesting! 00:06:06.796 --> 00:06:11.940 LU: Well, I don't know how she found out, and  anyway, so she was super, super helpful. 00:06:11.940 --> 00:06:15.480 HUIZINGA: OK, so go a little  further on this because I know   00:06:15.480 --> 00:06:17.320 you have others that have  influence you, as well. 00:06:17.320 --> 00:06:21.280 LU: Yes. Yes, yes. And I think those,  to be honest, I'm a very emotional,   00:06:21.280 --> 00:06:28.040 sensitive person. I would just, you know, move the  timeline to be, kind of, more recent. So I joined   00:06:28.040 --> 00:06:33.840 Microsoft Research as a manager, and there's  something called Connect that, you know, people   00:06:33.840 --> 00:06:39.920 write down twice every year talking about what  it is they’ve been doing. So I was just checking,   00:06:39.920 --> 00:06:45.920 you know, my members in my team to see what they  have been doing over the years just to just get   00:06:45.920 --> 00:06:53.840 myself familiar with them. And I remember I read  several of them. I felt like I almost have tears   00:06:53.840 --> 00:07:02.400 in my eyes! Like, I realized, wow, like … And  just to give example, for Chris, Chris Hawblitzel,   00:07:02.400 --> 00:07:08.160 I read his Connect, and I saw that he's working  on something called program verification. It's   00:07:08.160 --> 00:07:12.960 a very, very difficult problem, and [as an]  outsider, you know, I've read many of his papers,   00:07:12.960 --> 00:07:20.840 but when I read, you know, his own writing, and I  realized, wow, you know, it's almost two decades,   00:07:20.840 --> 00:07:29.240 right. Like, he just keeps doing these very  difficult things. And I read his words about, you   00:07:29.240 --> 00:07:36.160 know, how his old approach has problems, how he’s  thinking about how to address that problem. Oh, I   00:07:36.160 --> 00:07:42.360 have an idea, right. And then spend multiple years  to implement that idea and get improvement; find a   00:07:42.360 --> 00:07:49.920 new problem and then just find new solutions. And  I really feel like, wow, I'm really, really, like,   00:07:49.920 --> 00:07:56.080 I feel like this is, kind of, like a, you know,  there's, how to say, a hero-ish story behind this,   00:07:56.080 --> 00:08:02.400 you know, this kind of goal, and you're willing to  spend many years to keep tackling this challenging   00:08:02.400 --> 00:08:08.920 problem. And I just feel like, wow, I'm so  honored, you know, to be in the same group   00:08:08.920 --> 00:08:14.060 with a group of fighters, you know, determined  to tackle difficult research problems. 00:08:14.060 --> 00:08:18.760 HUIZINGA: Yeah. And I think when you talk about  it, it's like this is a person that was working   00:08:18.760 --> 00:08:24.400 for you, a direct report. [LAUGHTER] And often,  we think about our heroes as being the ones who   00:08:24.400 --> 00:08:30.916 mentored us, who taught us, who managed us,  but yours is kind of 360! It’s like … 00:08:30.916 --> 00:08:31.280 LU: True! 00:08:31.280 --> 00:08:33.560 HUIZINGA: … your heroes [are]  above, beside and below. 00:08:33.560 --> 00:08:39.240 LU: Right. And I would just say that I have many  other, you know, direct reports in my group,   00:08:39.240 --> 00:08:45.000 and I have, you know, for example, say a couple  other … my colleagues, my direct reports,   00:08:45.000 --> 00:08:50.760 Dan Ports and Jacob Nelson. And again, this  is something like their story really inspired   00:08:50.760 --> 00:08:55.400 me. Like, they were, again, spent five or  six years on something, and it looks like,   00:08:55.400 --> 00:08:59.560 oh, it's close to the success of tech  transfer, and then something out of   00:08:59.560 --> 00:09:05.480 their control happened. It happened because  Intel decided to stop manufacturing a chip   00:09:05.480 --> 00:09:11.493 that their research relied on. And it's, kind  of, like the end of the world to them, … 00:09:11.493 --> 00:09:11.512 HUIZINGA: Yeah. 00:09:11.512 --> 00:09:16.840 LU: … and then they did not give up. And  then, you know, like, one year later,   00:09:16.840 --> 00:09:20.400 they found a solution, you know, together  with their product team collaborators. 00:09:20.400 --> 00:09:21.060 HUIZINGA: Wow. 00:09:21.060 --> 00:09:24.840 LU: And I still feel like, wow, you  know, I feel so … I feel like I'm   00:09:24.840 --> 00:09:29.480 inspired every day! Like, I'm so happy  to be working together with, you know,   00:09:29.480 --> 00:09:33.280 all these great people, great  researchers in my team. 00:09:33.280 --> 00:09:40.520 HUIZINGA: Yeah. Wow. So much of your work  centers on this idea of concurrent systems   00:09:40.520 --> 00:09:44.960 and I want you to talk about some specific  examples of this work next, but I think it   00:09:44.960 --> 00:09:50.480 warrants a little explication upfront for those  people in the audience who don't spend all their   00:09:50.480 --> 00:09:56.880 time working on concurrent systems themselves. So  give us a short “101” on concurrent systems and   00:09:56.880 --> 00:10:03.020 explain why the work you do matters to both the  people who make it and the people who use it. 00:10:03.020 --> 00:10:06.640 LU: Sure. Yeah. So I think a lot of  people may not realize … so actually,   00:10:06.640 --> 00:10:13.240 the software we're using every day, almost every  software we use these days are concurrent. So the   00:10:13.240 --> 00:10:21.200 meaning of concurrent is that you have multiple  threads of execution going on at the same time,   00:10:21.200 --> 00:10:28.520 in parallel. And then, when we go to a web  browser, right, so it's not just one rendering   00:10:28.520 --> 00:10:33.880 that is going on. There are actually multiple  concurrent renderings that is going on. So the   00:10:33.880 --> 00:10:40.920 problem of writing … for software developers  to develop this type of concurrent system,   00:10:40.920 --> 00:10:46.320 a challenge is the timing. So because you  have multiple concurrent things going on,   00:10:46.320 --> 00:10:53.680 it's very difficult to manage and reason about,  you know, what may happen first, what may happen   00:10:53.680 --> 00:10:59.520 second. And also, it’s, like, there's an inherent  non-determinism in it. What happened first   00:10:59.520 --> 00:11:07.040 this time may happen second next time. So as a  result, a lot of bugs are introduced by this.   00:11:07.040 --> 00:11:12.920 And it was a very challenging problem because  I would say about 20 years ago, there was a   00:11:12.920 --> 00:11:20.000 shift. Like, in the older days, actually most  of our software is written in a sequential way   00:11:20.000 --> 00:11:25.880 instead of a concurrent way. So, you know, a  lot of developers also have a difficult time   00:11:25.880 --> 00:11:31.120 to shift their mindset from the sequential way of  reasoning to this concurrent way of reasoning. 00:11:31.120 --> 00:11:37.440 HUIZINGA: Right. Well, and I think, from a user's  perspective, all you experience is what I like   00:11:37.440 --> 00:11:44.360 to call the spinning beachball of doom. It's like  I've asked something, and it doesn't want to give,   00:11:44.360 --> 00:11:49.400 so [LAUGHS] ... And this is, like, behind  the scenes from a reasoning perspective of,   00:11:49.400 --> 00:11:53.520 how do we keep that from happening to our  users? How do we identify the bugs? Which   00:11:53.520 --> 00:12:00.320 we'll get to in a second. Umm. Thanks for  that. Your research now revolves around what   00:12:00.320 --> 00:12:05.960 I would call the big idea of learning from  mistakes. And in fact, it all seems to have   00:12:05.960 --> 00:12:11.800 started with a paper that you published way  back in 2008 called “Learning from Mistakes:   00:12:11.800 --> 00:12:18.440 A Comprehensive Study on Real World Concurrency  Bug Characteristics,” and you say this strongly   00:12:18.440 --> 00:12:25.560 influenced your research style and approach. And  by the way, I'll note that this paper received the   00:12:25.560 --> 00:12:32.120 Most Influential Paper Award in 2022 from ASPLOS,  which is the Architectural Support for Programming   00:12:32.120 --> 00:12:38.360 Languages and Operating Systems. Huge mouthful.  And it also has more than a thousand citations,   00:12:38.360 --> 00:12:45.520 so I dare say it's influenced other researchers’  approach to research, as well. Talk about the big   00:12:45.520 --> 00:12:51.548 idea behind this paper and exactly how it informed  your research style and approach today. 00:12:51.548 --> 00:12:56.280 LU: Mm-hmm. Yeah. So I think this, like,  again, went back to the days that I, you know,   00:12:56.280 --> 00:13:02.160 my PhD days, I started working with my adviser,  you know, YY (Yuanyuan Zhou). So at that time,   00:13:02.160 --> 00:13:07.040 there had been a lot of people working on bug  finding, but then now when I think about it,   00:13:07.040 --> 00:13:11.440 people just magically say, hey, I want to  look at this type of bug. Just magically,   00:13:11.440 --> 00:13:17.560 oh, I want to look at that type of bug. And then,  my adviser at that time suggested to me, saying,   00:13:17.560 --> 00:13:22.320 hey, maybe, you know, actually take a look, right.  At that time, as I mentioned, software was kind of   00:13:22.320 --> 00:13:27.360 shifting from sequential software to concurrent  software, and my adviser was saying, hey, just   00:13:27.360 --> 00:13:34.680 take a look at those real systems bug databases,  and see what type of concurrency bugs are actually   00:13:34.680 --> 00:13:38.800 there. You know, instead of just randomly saying,  oh, I want to work on this type of bug. 00:13:38.800 --> 00:13:39.960 HUIZINGA: Oh, yeah. 00:13:39.960 --> 00:13:44.920 LU: And then also, of course, it's not just look  at it. It's not just like you read a novel or   00:13:44.920 --> 00:13:49.680 something, right. [LAUGHTER] And again, my adviser  said, hey, Shan, right, you have this, you have   00:13:49.680 --> 00:13:56.270 a connection, natural connection, you know,  with bugs and the developers who commit … 00:13:56.270 --> 00:13:57.410 HUIZINGA: Who make them … 00:13:57.410 --> 00:14:00.160 LU: Who make them! [LAUGHTER] So she  said, you know, try to think about the   00:14:00.160 --> 00:14:04.790 patterns behind them, right. Try to think  about whether you can generalize some … 00:14:04.790 --> 00:14:04.992 HUIZINGA: Interesting … 00:14:04.992 --> 00:14:09.520 LU: … characteristics, and use that  to guide people's research in this   00:14:09.520 --> 00:14:14.560 domain. And at that time, we were actually  thinking we don't know whether, you know,   00:14:14.560 --> 00:14:19.200 we can actually write a paper about it because  traditionally you publish a paper, just say,   00:14:19.200 --> 00:14:24.560 oh, I have a new tool, right, which can do this  and that. At that time in system conferences,   00:14:24.560 --> 00:14:30.200 people rarely have, you know, just say, here's  a study, right. But we studied that, and indeed,   00:14:30.200 --> 00:14:37.080 you know, I had this thought that, hey, why  I make a lot of mistakes. And when I study a   00:14:37.080 --> 00:14:42.240 lot of bugs, the more and more, I feel, you know,  there's a reason behind it, right. It's like I'm   00:14:42.240 --> 00:14:48.400 not the only dumb person in the world, right?  [LAUGHTER] There's a reason that, you know,   00:14:49.280 --> 00:14:54.040 there's some part of this language is difficult  to use, right, and there's a certain type of   00:14:54.040 --> 00:14:59.440 concurrent reasoning, it’s just not natural  to many people, right. So because of that,   00:14:59.440 --> 00:15:05.200 there are patterns behind these bugs. And so at  that time, we were surprised that the paper was   00:15:05.200 --> 00:15:12.080 actually accepted. Because I'm just happy with the  learning I get. But after this paper was accepted,   00:15:12.920 --> 00:15:18.320 in the next, I would say, many years, there  are more and more people realize, hey, before   00:15:18.320 --> 00:15:24.400 we actually, you know, do bug-finding things,  let's first do a study, right, to understand,   00:15:24.400 --> 00:15:28.960 and then this paper was … yeah … I was very  happy that it was cited many, many times. 00:15:28.960 --> 00:15:33.720 HUIZINGA: Yeah. And then gets the most  influential paper many years later. 00:15:33.720 --> 00:15:35.360 LU: Many years later. Yes. 00:15:35.360 --> 00:15:40.200 HUIZINGA: Yeah, I feel like there's a lot  of things going through my head right now,   00:15:40.200 --> 00:15:43.680 one of which is what AI is, is a pattern detector,   00:15:43.680 --> 00:15:49.520 and you were doing that before AI even came on  the scene. Which goes to show you that humans   00:15:49.520 --> 00:15:53.493 are pretty good at pattern detection  also. We might not do as fast as … 00:15:53.493 --> 00:15:53.506 LU: True. 00:15:53.506 --> 00:15:58.920 HUIZINGA: … as an AI but … so this  idea of learning from mistakes   00:15:59.880 --> 00:16:06.640 is a broad theme. Another theme that I see  coming through your papers and your work is   00:16:06.640 --> 00:16:11.520 persistence. [LAUGHTER] And you mentioned  this about your team, right. I was like,   00:16:11.520 --> 00:16:20.320 these people are people who don't give up. So we  covered this idea in an Abstracts podcast recently   00:16:20.320 --> 00:16:26.240 talking about a paper which really brings this  to light: “If at First You Don't Succeed, Try,   00:16:26.240 --> 00:16:31.120 Try Again.” That's the name of the paper. And we  didn't have time to discuss it in depth at the   00:16:31.120 --> 00:16:36.200 time because the Abstracts show is so quick. But  we do now. So I'd like you to expand a little bit   00:16:36.200 --> 00:16:42.640 on this big idea of persistence and how large  language models are not only changing the way   00:16:42.640 --> 00:16:49.880 programming and verification happens but also  providing insights into detecting retry bugs. 00:16:49.880 --> 00:16:54.800 LU: Yes. So I guess maybe I will, since  you mentioned this persistence, you know,   00:16:54.800 --> 00:17:02.160 after that “Learning from Mistakes” paper—so that  was in 2008—and in the next 10 years, a little   00:17:02.160 --> 00:17:08.280 bit more than 10 years, in terms of persistence,  right, so we have continued, me and my students,   00:17:08.280 --> 00:17:12.430 my collaborators, we have continued working  on, you know, finding concurrency bugs … 00:17:12.430 --> 00:17:12.960 HUIZINGA: Yeah. 00:17:12.960 --> 00:17:17.080 LU: … which is related to, kind of related to,  why I'm here at Microsoft Research. And we keep   00:17:17.080 --> 00:17:23.880 doing it, doing it, and then I feel like a high  point was that I had a collaboration with my now   00:17:23.880 --> 00:17:33.040 colleagues here, Madan Musuvathi and Suman Nath.  So we built a tool to detect concurrency bugs,   00:17:33.040 --> 00:17:38.640 and after more than 15 years of effort  on this, we were able to find more than   00:17:38.640 --> 00:17:46.640 1,000 concurrency bugs. It was built in a tool  called Torch that was deployed in the company,   00:17:46.640 --> 00:17:52.280 and it won the Best Paper Award at  the top system conference, SOSP,   00:17:52.280 --> 00:18:01.921 and it was actually a bittersweet moment.  This paper seems to, you know, put an end … 00:18:01.921 --> 00:18:01.952 HUIZINGA: Oh, interesting! 00:18:01.952 --> 00:18:09.800 LU: … to our research. And also some of the  findings from that paper is that we used to   00:18:09.800 --> 00:18:16.280 do very sophisticated program analysis to  reason about the timing. And in that paper,   00:18:16.280 --> 00:18:19.360 we realized actually, sometimes,  if you’re a little bit fuzzy,   00:18:19.360 --> 00:18:28.760 don't aim to do perfect analysis, the resulting  tool is actually more effective. So after that   00:18:29.480 --> 00:18:34.760 paper, Madan, Suman, and me, we kind of, you  know, shifted our focus to looking at other   00:18:34.760 --> 00:18:42.120 types of bugs. And at the same time, the three of  us realized the traditional, very precise program   00:18:42.120 --> 00:18:52.240 analysis may not be needed for some of the bug  finding. So then, for this paper, this retry bugs,   00:18:52.240 --> 00:18:56.720 after we shifted our focus away from concurrency  bugs, we realized, oh, there are many other types   00:18:56.720 --> 00:19:03.120 of important bugs, such as, in this case, like  retry, right, when your software goes wrong,   00:19:03.120 --> 00:19:07.840 right. Another thing we learned is that it  looks like you can never eliminate all bugs,   00:19:07.840 --> 00:19:13.000 so something will go wrong, [LAUGHTER] and then  so that's why you need something like retry,   00:19:13.000 --> 00:19:18.056 right. So like if something goes wrong,  at least you won't give up immediately. 00:19:18.056 --> 00:19:18.076 HUIZINGA: Right. 00:19:18.076 --> 00:19:22.840 LU: The software will retry. And another thing  that started from this earlier effort is we   00:19:22.840 --> 00:19:28.200 started using large language models because we  realized, yeah, you know, traditional program   00:19:28.200 --> 00:19:34.880 analysis sometimes can give you a very strong  guarantee, but in some other cases, like in this   00:19:34.880 --> 00:19:42.940 retry case, some kind of fuzzy analysis, you know,  not so precise, offered by large language models   00:19:42.940 --> 00:19:51.206 is sometimes even more beneficial. Yeah. So that's  kind of, you know, the story behind this paper. 00:19:51.206 --> 00:19:55.760 HUIZINGA: Yeah, yeah, yeah, yeah. So, Shan, we're  hearing a lot about how large language models are   00:19:55.760 --> 00:20:03.720 writing code nowadays. In fact, NVIDIA's CEO says,  mamas, don't let your babies grow up to be coders   00:20:03.720 --> 00:20:07.920 because AI’s going to do that. I don't know if  he's right, but one of the projects you're most   00:20:07.920 --> 00:20:13.920 excited about right now is called Verus, and your  colleague Jay Lorch recently said that he sees a   00:20:13.920 --> 00:20:19.720 lot of synergy between AI and verification, where  each discipline brings something to the other,   00:20:19.720 --> 00:20:25.960 and Rafah Hosn has referred to this as  “co-innovation” or “bidirectional enrichment.”   00:20:25.960 --> 00:20:30.920 I don't know if that's exactly what is going on  here, but it seems like it is. Tell us more about   00:20:30.920 --> 00:20:36.340 this project, Verus, and how AI and software  verification are helping each other out. 00:20:36.340 --> 00:20:40.920 LU: Yes, yes, yes, yes. I'm very excited  about this project now! So first of all,   00:20:40.920 --> 00:20:45.640 starting from Verus. So Verus is a tool  that helps you verify the correctness   00:20:45.640 --> 00:20:51.560 of Rust code. So this is a … it’s a relatively  new tool, but it’s creating a lot of, you know,   00:20:51.560 --> 00:20:56.800 excitement in the research community,  and it’s created by my colleague Chris   00:20:56.800 --> 00:21:00.120 Hawblitzel and his collaborators  outside Microsoft Research. 00:21:00.120 --> 00:21:00.960 HUIZINGA: Interesting. 00:21:00.960 --> 00:21:05.280 LU: And as I mentioned, right, this is a  part that, you know, really inspired me.   00:21:05.280 --> 00:21:10.920 So traditionally to verify, right, your  program is correct, it requires a lot of   00:21:10.920 --> 00:21:17.960 expertise. You actually have to write your proof  typically in a special language. And, you know,   00:21:17.960 --> 00:21:23.960 so a lot of people, including me, right, who  are so eager to get rid of bugs in my software,   00:21:23.960 --> 00:21:29.600 but there are people told me, saying just to learn  that language—so they were referring to a language   00:21:29.600 --> 00:21:35.080 called Coq—just to learn that language,  they said it takes one or two years. And   00:21:35.080 --> 00:21:39.520 then once you learn that language, right, then  you have to learn about how to write proofs in   00:21:39.520 --> 00:21:45.400 that special language. So people, particularly in  the bug-finding community, people know that, oh,   00:21:45.400 --> 00:21:51.760 in theory, you can verify it, but in reality,  people don't do that. OK, so now going back   00:21:51.760 --> 00:21:58.880 to this Verus tool, why it's exciting … so it  actually allows people to write proofs in Rust.   00:21:58.880 --> 00:22:05.680 So Rust is an increasingly popular language.  And there are more and more people picking up   00:22:05.680 --> 00:22:10.880 Rust. It’s the first time I heard about, oh,  you can, you know, write proofs in a popular   00:22:10.880 --> 00:22:21.760 language. And also, another thing is in the past,  you cannot verify an implementation directly. You   00:22:21.760 --> 00:22:28.160 can only verify something written in a special  language. And the proof is proving something   00:22:28.160 --> 00:22:35.000 that is in a special language. And then finally,  that special language is maybe then transformed   00:22:35.000 --> 00:22:40.901 into an implementation. So it's just, there's  just too many special languages there. 00:22:40.901 --> 00:22:44.040 HUIZINGA: A lot of layers. LU: A lot of layers. So now this Verus tool allows 00:22:44.040 --> 00:22:51.520 you to write a proof in Rust to prove an  implementation that is in Rust. So it's   00:22:51.520 --> 00:22:55.440 very direct. I just feel like I'm just  not good at learning a new language. 00:22:55.440 --> 00:22:56.360 HUIZINGA: Interesting. 00:22:56.360 --> 00:23:00.000 LU: So when I came here, you know, and  learned about this Verus tool, you know,   00:23:00.000 --> 00:23:07.080 by Chris and his collaborators, I feel like,  oh, looks like maybe I can give it a try.   00:23:07.080 --> 00:23:14.380 And surprisingly, I realized, oh, wow! I can  actually write proofs using this Verus tool. 00:23:14.380 --> 00:23:14.940 HUIZINGA: Right. 00:23:14.940 --> 00:23:19.080 LU: And then, of course, you know, I  was told, if you really want to, right,   00:23:19.080 --> 00:23:25.960 write proofs for large systems, it still takes a  lot of effort. And then this idea came to me that,   00:23:25.960 --> 00:23:30.120 hey, maybe, you know, these days, like,  large language models can write code,   00:23:30.120 --> 00:23:33.680 then why not let large language models  write proofs, right? And of course,   00:23:33.680 --> 00:23:38.920 you know, other people actually had this idea,  as well, but there's a doubt that, you know,   00:23:38.920 --> 00:23:43.280 can large language models really write proofs,  right? And also, people have this feeling that,   00:23:43.280 --> 00:23:51.320 you know, large language models seem not very  disciplined, you know, by nature. But, you know,   00:23:51.320 --> 00:23:58.600 that's what intrigued me, right. And also, I used  to be a doubter for, say, GitHub Copilot. USED   00:23:58.600 --> 00:24:05.550 to! Because I feel like, yes, it can generate  a lot of code, but who knows [LAUGHS] … 00:24:05.550 --> 00:24:06.516 HUIZINGA: Whether it's right … 00:24:06.516 --> 00:24:07.760 LU: What, what is … whether it's right? 00:24:07.760 --> 00:24:08.200 HUIZINGA: Yeah. 00:24:08.200 --> 00:24:11.560 LU: Right, so I feel like, wow, you know,  this could be a game-changer, right? Like,   00:24:11.560 --> 00:24:16.920 if AI can write not only code but also  proofs. Yeah, so that's what I have been   00:24:16.920 --> 00:24:23.240 doing. I've been working on this for one year,  and I gradually get more collaborators both,   00:24:23.240 --> 00:24:30.160 you know, people in Microsoft Research Asia,  and, you know, expertise here, like Chris,   00:24:30.160 --> 00:24:34.640 and Jay Lorch. They all help me a lot. So  we actually have made a lot of progress. 00:24:34.640 --> 00:24:35.200 HUIZINGA: Yeah. 00:24:35.200 --> 00:24:41.240 LU: Like, now it's, like, we've tried,  like, for example, for some small programs,   00:24:41.240 --> 00:24:46.520 benchmarks, and we see that actually large  language models can correctly prove the   00:24:46.520 --> 00:24:51.100 majority of the benchmarks that we throw  to it. Yeah. It's very, very exciting. 00:24:51.100 --> 00:24:54.560 HUIZINGA: Well, and so … and we're  going to talk a little bit more about   00:24:54.560 --> 00:24:58.320 some of those doubts and some  of those interesting concerns   00:24:59.000 --> 00:25:06.480 in a bit. I do want you to address what I think  Jay was getting at, which is that somehow the   00:25:06.480 --> 00:25:12.620 two help each other. The verification improves  the AI. The AI improves the verification. 00:25:12.620 --> 00:25:13.750 LU: Yes, yes. 00:25:13.750 --> 00:25:14.120 HUIZINGA: How? 00:25:14.120 --> 00:25:20.840 LU: Yes. My feeling is that a lot of people, if  they're concerned with using AI, it’s because they   00:25:20.840 --> 00:25:26.760 feel like there's no guarantee for the content  generated by AI, right. And then we also all   00:25:26.760 --> 00:25:31.560 heard about, you know, hallucination.  And I tried myself. Like, I remember,   00:25:31.560 --> 00:25:36.920 at some point, if I ask AI, say,  you know, which is bigger: is it   00:25:36.920 --> 00:25:44.104 three times three or eight? And the AI will  tell me eight is bigger. And … [LAUGHTER] 00:25:44.104 --> 00:25:44.660 HUIZINGA: Like, what? 00:25:44.660 --> 00:25:48.950 LU: So I feel like verification  can really help AI … 00:25:48.950 --> 00:25:50.520 HUIZINGA: Get better … 00:25:50.520 --> 00:25:58.240 LU: … because now you can give, you know,  kind of, add in mathematical rigors into   00:25:59.160 --> 00:26:03.480 whatever that is generated by AI, right.  And I say it would help AI. It will also   00:26:03.480 --> 00:26:11.376 help people who use AI, right, so that  they know what can be trusted, right. 00:26:11.376 --> 00:26:11.396 HUIZINGA: Right. 00:26:11.396 --> 00:26:14.560 LU: What is guaranteed by this  content generated by AI? 00:26:14.560 --> 00:26:15.260 HUIZINGA: Yeah, yeah, yeah. 00:26:15.260 --> 00:26:18.000 LU: Yeah, and now of course AI can  help verification because, you know,   00:26:18.000 --> 00:26:23.880 verification, you know, it's hard. There  is a lot of mathematical reasoning behind   00:26:23.880 --> 00:26:30.680 it. [LAUGHS] And so now with AI, it  will enable verification to be picked   00:26:30.680 --> 00:26:37.180 up by more and more developers so that  we can get higher-quality software. 00:26:37.180 --> 00:26:38.577 HUIZINGA: Yeah. 00:26:38.577 --> 00:26:38.590 LU: Yeah. 00:26:38.590 --> 00:26:42.920 HUIZINGA: Yeah. And we'll get to that, too,  about what I would call the democratization of   00:26:42.920 --> 00:26:50.400 things. But before that, I want to, again, say an  observation that I had based on your work and my   00:26:50.400 --> 00:26:54.760 conversations with you is that you've basically  dedicated your career to hunting bugs. 00:26:54.760 --> 00:26:55.480 LU: Yes. 00:26:55.480 --> 00:27:00.480 HUIZINGA: And maybe that's partly  due to a personal story about how a   00:27:00.480 --> 00:27:04.457 tiny mistake became a bug that haunted  you for years. Tell us the story. 00:27:04.457 --> 00:27:04.470 LU: Yes. 00:27:04.470 --> 00:27:09.160 HUIZINGA: And explain why and how it  launched a lifelong quest to understand,   00:27:09.160 --> 00:27:12.120 detect, and expose bugs of all kinds. 00:27:12.120 --> 00:27:16.800 LU: Yes. So before I came here, I  already had multiple times, you know,   00:27:16.800 --> 00:27:19.160 interacting with Microsoft Research. So I was a   00:27:19.160 --> 00:27:23.374 summer intern at Microsoft Research  Redmond almost 20 years ago. 00:27:23.374 --> 00:27:23.396 HUIZINGA: Oh, wow! 00:27:23.396 --> 00:27:30.040 LU: I think it was in the summer of 2005.  And I remember I came here, you know,   00:27:30.040 --> 00:27:37.320 full of ambition. And I thought, OK, you know,  I will implement some smart algorithm. I will   00:27:37.320 --> 00:27:44.360 deliver some useful tools. So at that time, I had  just finished two years of my PhD, so I, kind of,   00:27:44.360 --> 00:27:51.240 just started my research on bug finding and so on.  And I remember I came here, and I was told that   00:27:51.240 --> 00:27:58.120 I need to program in C#. And, you know, I just  naturally have a fear of learning a new language.   00:27:58.960 --> 00:28:05.760 But anyway, I remember, I thought, oh, the task I  was assigned was very straightforward. And I think   00:28:05.760 --> 00:28:11.160 I went ahead of myself. I was thinking, oh, I want  to quickly finish this, and I want to do something   00:28:11.160 --> 00:28:19.160 more novel, you know, that can be more creative.  But then this simple task I was assigned,   00:28:19.160 --> 00:28:26.920 I ended up spending the whole summer on it. So  the tool that I wrote was supposed to process very   00:28:26.920 --> 00:28:32.960 huge logs. And then the problem is my software is,  like, you run it initially … So, like, I can only   00:28:32.960 --> 00:28:41.520 run it for 10 minutes because my software used so  much memory and it will crash. And then, I spent a   00:28:41.520 --> 00:28:46.120 lot of time … I was thinking, oh, my software is  just using too much memory. Let me optimize it,   00:28:46.120 --> 00:28:51.800 right. And then so, I, you know, I try to make  sure to use memory in a very efficient way,   00:28:51.800 --> 00:28:58.360 but then as a result, instead of crashing every  10 minutes, it will just crash after one hour. And   00:28:58.360 --> 00:29:03.520 I know there's a bug at that time. So there's a  type of bug called memory leak. I know there's a   00:29:03.520 --> 00:29:09.680 bug in my code, and I spent a lot of time and  there was an engineer helping me checking my   00:29:09.680 --> 00:29:16.160 code. We spent a lot of time. We were just  not able to find that bug. And at the end,   00:29:16.160 --> 00:29:26.040 we … the solution is I was just sitting in front  of my computer waiting for my program to crash and   00:29:26.040 --> 00:29:34.000 restart. [LAUGHTER] And at that time, because  there was very little remote working option,   00:29:34.000 --> 00:29:38.910 so in order to finish processing all those  logs, it's like, you know, after dinner, I … 00:29:38.910 --> 00:29:40.100 HUIZINGA: You have to stay all night! 00:29:40.100 --> 00:29:44.840 LU: I have to stay all night! And all  my intern friends, they were saying, oh,   00:29:44.840 --> 00:29:49.440 Shan, you work really hard!  And I'm just feeling like,   00:29:49.440 --> 00:29:52.520 you know what I'm doing is just sitting in  front of my computer waiting [LAUGHTER] for   00:29:52.520 --> 00:30:00.080 my program to crash so that I can restart  it! And near the end of my internship,   00:30:00.080 --> 00:30:09.640 I finally find the bug. It turns out that I  missed a pair of brackets in one line of code. 00:30:09.640 --> 00:30:11.851 HUIZINGA: That's it. 00:30:11.851 --> 00:30:12.960 LU: That's it. HUIZINGA: Oh, my goodness. 00:30:12.960 --> 00:30:20.360 LU: And it turns out, because I was used to C,  and in C, when you want to free, which means   00:30:20.360 --> 00:30:29.640 deallocate, an array, you just say “free array.”  And if I remember correctly, in this language,   00:30:29.640 --> 00:30:35.520 C#, you have to say, “free this array name”  and you put a bracket behind it. Otherwise,   00:30:35.520 --> 00:30:44.680 it will only free the first element. And I  … it was a nightmare. And I also felt like,   00:30:44.680 --> 00:30:49.093 the most frustrating thing is, if  it's a clever bug, right … [LAUGHS] 00:30:49.093 --> 00:30:49.112 HUIZINGA: Sure. 00:30:49.112 --> 00:30:53.176 LU: … then you feel like at least I'm  defeated by something complicated … 00:30:53.176 --> 00:30:53.196 HUIZINGA: Smart. 00:30:53.196 --> 00:30:58.680 LU: Something smart. And then it's like, you  know, also all this ambition I had about,   00:30:58.680 --> 00:31:03.520 you know, doing creative work, right,  with all these smart researchers in   00:31:03.520 --> 00:31:10.020 MSR (Microsoft Research), I feel like I ended up  achieving very little in my summer internship. 00:31:10.020 --> 00:31:19.160 HUIZINGA: But maybe the humility of making a  stupid mistake is the kind of thing that somebody   00:31:19.160 --> 00:31:26.360 who's good at hunting bugs … It's like missing an  error in the headline of an article, because the   00:31:26.360 --> 00:31:30.440 print is so big [LAUGHTER] that you're looking  for the little things in the … I know that's   00:31:30.440 --> 00:31:37.160 a journalist's problem. Actually, I actually  love that story. And it, kind of, presents a   00:31:37.160 --> 00:31:45.040 big picture of you, Shan, as a person who has  a realistic, self-awareness of … and humility,   00:31:45.040 --> 00:31:53.000 which I think is rare at times in the software  world. So thanks for sharing that. So moving   00:31:53.000 --> 00:31:59.040 on. When we talked before, you mentioned the large  variety of programming languages and how that can   00:31:59.040 --> 00:32:05.160 be a barrier to entry or at least a big hurdle to  overcome in software programming and verification.   00:32:05.160 --> 00:32:10.116 But you also talked about, as we just mentioned,  how LLMs have been a democratizing force … 00:32:10.116 --> 00:32:10.306 LU: Yes. 00:32:10.306 --> 00:32:14.076 HUIZINGA: … in this field. So going  back to when you first started … 00:32:14.076 --> 00:32:14.386 LU: Yes. 00:32:14.386 --> 00:32:19.476 HUIZINGA: … and what you see now with the  advent of tools like GitHub Copilot, … 00:32:19.476 --> 00:32:20.026 LU: Yes. 00:32:20.026 --> 00:32:21.280 HUIZINGA: … what … what's changed? 00:32:21.280 --> 00:32:26.000 LU: Oh, so much has changed. Well, I  don't even know how to start. Like,   00:32:26.000 --> 00:32:33.360 I used to be really scared about programming. You  know, when I tell this story, a lot of people say,   00:32:33.360 --> 00:32:37.760 no, I don't believe you. And I feel  like it's a trauma, you know. 00:32:37.760 --> 00:32:38.127 HUIZINGA: Sure. 00:32:38.127 --> 00:32:47.680 LU: I almost feel like it's like, you know,  the college-day me, right, who was scared of   00:32:47.680 --> 00:32:54.480 starting any programming project. Somehow,  I felt humiliated when asking those very,   00:32:54.480 --> 00:33:01.120 I feel like, stupid questions to my classmates.  It almost changed my personality! It’s like … for   00:33:01.120 --> 00:33:07.320 a long time, whenever someone introduced me to  a new software tool, my first reaction is, uh,   00:33:07.320 --> 00:33:12.320 I probably will not be able to successfully  even install it. Like whenever, you know,   00:33:12.320 --> 00:33:19.320 there's a new language, my first reaction  is, uh, no, I'm not good at it. And then,   00:33:19.320 --> 00:33:23.040 like, for example, this GitHub Copilot  thing, actually, I did not try it until   00:33:23.040 --> 00:33:29.400 I joined Microsoft. And then I, actually, I  haven't programmed for a long time. And then   00:33:29.400 --> 00:33:36.040 I started collaborating with people in Microsoft  Research Asia, and he writes programs in Python,   00:33:36.040 --> 00:33:45.760 right. And I have never written a single line of  Python code before. And also, this Verus tool. It   00:33:45.760 --> 00:33:54.320 helps you to verify code in Rust, but I have never  learned Rust before. So I thought, OK, maybe let   00:33:54.320 --> 00:34:01.830 me just try GitHub Copilot. And wow! You know,  it's like I realized, wow! Like … [LAUGHS] 00:34:01.830 --> 00:34:02.380 HUIZINGA: I can do this! 00:34:02.380 --> 00:34:07.680 LU: I can do this! And, of course, sometimes  I feel like my colleagues may sometimes be   00:34:07.680 --> 00:34:12.200 surprised because on one hand it looks  like I'm able to just finish, you know,   00:34:12.200 --> 00:34:19.000 write a Rust function. But on some other days, I  ask very basic questions, [LAUGHTER] and I have   00:34:19.000 --> 00:34:23.470 those questions because, you know, the GitHub  Copilot just helps me finish! [LAUGHS] 00:34:23.470 --> 00:34:23.600 HUIZINGA: Right. 00:34:23.600 --> 00:34:27.720 LU: You know, I’m just starting something to  start it, and then it just helps me finish.   00:34:28.720 --> 00:34:35.040 And I wish, when I started my college,  if at that time there was GitHub Copilot,   00:34:35.040 --> 00:34:39.160 I feel like, you know, my mindset  towards programming and towards   00:34:39.160 --> 00:34:45.280 computer science might be different. So it  does make me feel very positive, you know,   00:34:46.000 --> 00:34:52.620 about, you know, what future we have, you  know, with AI, with computer science. 00:34:52.620 --> 00:34:57.840 HUIZINGA: OK, usually, I ask researchers  at this time, what could possibly go wrong   00:34:57.840 --> 00:35:02.640 if you got everything right? And I was  thinking about this question in a different   00:35:02.640 --> 00:35:11.040 way until just this minute. I want to ask  you … what do you think that it means to   00:35:11.040 --> 00:35:19.160 have a tool that can do things for you that  you don't have to struggle with? And maybe,   00:35:19.160 --> 00:35:26.107 is there anything good about the struggle? Because  you're framing it as it sapped your confidence. 00:35:26.107 --> 00:35:26.380 LU: [LAUGHS] Yes. 00:35:26.380 --> 00:35:30.640 HUIZINGA: And at the same time, I  see a woman who emerged stronger   00:35:30.640 --> 00:35:35.960 because of this struggle with an amazing  career, a huge list of publications,   00:35:35.960 --> 00:35:43.172 influential papers, citations, leadership  role. [LAUGHTER] So in light of that … 00:35:43.172 --> 00:35:43.186 LU: Right. 00:35:43.186 --> 00:35:46.280 HUIZINGA: … what do you see as the  tension between struggling to learn   00:35:46.280 --> 00:35:49.720 a new language versus having this  tool that can just do it that makes   00:35:49.720 --> 00:35:54.720 you look amazing? And maybe the  truth of it is you don't know! 00:35:54.720 --> 00:36:01.600 LU: Yeah. That's a very good point. I guess you  need some kind of balance. And on one hand, yes,   00:36:01.600 --> 00:36:06.960 I feel like, again, right, this goes back to  like my internship. I left with the frustration   00:36:06.960 --> 00:36:14.040 that I felt like I have so much creativity to  contribute, and yet I could not because of this   00:36:14.040 --> 00:36:19.160 language barrier. You know, I feel positive  in the sense that just from GitHub Copilot,   00:36:19.160 --> 00:36:25.080 right, how it has enabled me to just bravely try  something new. I feel like this goes beyond just   00:36:25.080 --> 00:36:32.080 computer science, right. I can imagine it'll  help people to truly unleash their creativity,   00:36:32.080 --> 00:36:38.760 not being bothered by some challenges in  learning the tool. But on the other hand,   00:36:38.760 --> 00:36:45.120 you made a very good point. My adviser told me  she feels like, you know, I write code slowly,   00:36:45.120 --> 00:36:53.600 but I tend to make fewer mistakes.  And the difficulty of learning, right,   00:36:53.600 --> 00:37:04.520 and all these nightmares I had definitely made  me more … more cautious? I pay more respect   00:37:05.280 --> 00:37:13.400 to the task that is given to me, so there is  definitely the other side of AI, right, which is,   00:37:13.400 --> 00:37:20.160 you feel like everything is easy and maybe you  do not have the experience of those bugs, right,   00:37:20.160 --> 00:37:26.337 that a software can bring to you and you  have overreliance, right, on this tool. 00:37:26.337 --> 00:37:26.356 HUIZINGA: Yeah! 00:37:26.356 --> 00:37:29.640 LU: So hopefully, you know, some  of the things we we're doing now,   00:37:29.640 --> 00:37:31.800 right, like for example, say verification, right,   00:37:31.800 --> 00:37:38.120 like bringing this mathematical rigor  to AI, hopefully that can help. 00:37:38.120 --> 00:37:45.160 HUIZINGA: Yeah. You know, even as you  unpack the nuances there, it strikes me   00:37:45.160 --> 00:37:51.036 that both are good. Both having to struggle  and learning languages and understanding … 00:37:51.036 --> 00:37:51.400 LU: Yeah. 00:37:51.400 --> 00:37:58.080 HUIZINGA: … the core of it and the idea that  in natural language, you could just say,   00:37:58.080 --> 00:38:06.880 here's what I want to happen, and the AI does  the code, the verification, etc. That said,   00:38:06.880 --> 00:38:12.480 do we trust it? And this was where I was going  with the first “what could possibly go wrong?”   00:38:12.480 --> 00:38:20.676 question. How do we know that it is really  as clever as it appears to be? [LAUGHS] 00:38:20.676 --> 00:38:24.200 LU: Yeah, I think I would just use the  research problem we are working on now,   00:38:24.200 --> 00:38:27.440 right. Like, I think on one hand, I can use AI   00:38:28.040 --> 00:38:35.840 to generate a proof, right, to prove the code  generated by AI is correct. But having said that,   00:38:35.840 --> 00:38:41.920 even if we're wildly successful, you know, in  this thing, human beings’ expertise is still   00:38:41.920 --> 00:38:47.960 needed because just take this as an example.  What do you mean by “correct,” right? 00:38:47.960 --> 00:38:48.290 HUIZINGA: Sure. 00:38:48.290 --> 00:38:55.000 LU: And so someone first has to define  what correctness means. And then so far,   00:38:55.000 --> 00:39:00.120 the experience shows that you can't just  define it using natural language because   00:39:00.120 --> 00:39:03.040 our natural language is inherently imprecise. 00:39:03.040 --> 00:39:03.960 HUIZINGA: Sure. 00:39:03.960 --> 00:39:13.080 LU: So you still need to translate it to a formal  specification in a programming language. It could   00:39:13.080 --> 00:39:20.160 be in a popular language like in Rust, right,  which is what Verus is aiming at. And then we are,   00:39:20.160 --> 00:39:23.680 like, for example, some of the research  we do is showing that, yes, you know,   00:39:23.680 --> 00:39:30.160 I can also use AI to do this translation from  natural language to specification. But again,   00:39:30.160 --> 00:39:36.880 then, who to verify that, right? So at the end of  the day, I think we still do need to have humans   00:39:36.880 --> 00:39:45.400 in the loop. But what we can do is to lower the  burden and make the interface not so complicated,   00:39:45.400 --> 00:39:51.880 right. So that it'll be easy for human  beings to check what AI has been doing. 00:39:51.880 --> 00:39:58.160 HUIZINGA: Yeah. You know, everything we're talking  about just reinforces this idea that we're living   00:39:58.160 --> 00:40:04.160 in a time where the advances in computer  science that seemed unrealistic or impossible,   00:40:04.160 --> 00:40:10.440 unattainable even a few years ago are now  so common that we take it for granted. And   00:40:10.440 --> 00:40:17.760 they don't even seem outrageous, but they are.  So I'm interested to know what, if anything,   00:40:17.760 --> 00:40:23.200 you would classify now as “blue sky” research in  your field. Maybe something in systems research   00:40:23.200 --> 00:40:30.200 today that looks like a moonshot. You've actually  anchored this in the fact that you, kind of, have,   00:40:30.200 --> 00:40:33.720 you know, blinders on for the work you're  doing—head down in the in the work you're   00:40:33.720 --> 00:40:41.360 doing—but even as you peek up from the work  that might be outrageous, is there anything   00:40:41.360 --> 00:40:46.420 else? I just like to get this out there that, you  know, what's going on 10 years down the line? 00:40:46.420 --> 00:40:53.600 LU: You know, sometimes I feel like I'm just  now so much into my own work, but, you know,   00:40:53.600 --> 00:40:59.800 occasionally, like, say, when I had a chat with  my daughter and I explained to her, you know, oh,   00:40:59.800 --> 00:41:05.680 I'm working on, you know, not only having AI to  generate code but also having AI to prove, right,   00:41:05.680 --> 00:41:11.920 the code is correct. And she would feel, wow,  that sounds amazing! [LAUGHS] So I don't know   00:41:11.920 --> 00:41:19.653 whether that is, you know, a moonshot thing, but  that's a thing that I'm super excited about … 00:41:19.653 --> 00:41:19.672 HUIZINGA: Yeah. 00:41:19.672 --> 00:41:21.920 LU: … about the potential. And  then there also have, you know,   00:41:21.920 --> 00:41:27.240 my colleagues, we spend a lot of time building  systems, and it's not just about correctness,   00:41:27.920 --> 00:41:32.920 right. Like, the verification thing I'm doing  now is related to automatically verify it’s   00:41:32.920 --> 00:41:37.640 correct. But also, you need to do a lot of  performance tuning, right. Just so that your   00:41:37.640 --> 00:41:46.320 system can react fast, right. It can have  good utilization of computer resources. And   00:41:46.320 --> 00:41:54.400 my colleagues are also working on using AI, right,  to automatically do performance tuning. And I know   00:41:54.400 --> 00:41:59.760 what they are doing, so I don't particularly  feel that's a moonshot, but I guess … 00:41:59.760 --> 00:42:03.360 HUIZINGA: I feel like, because you are so   00:42:03.360 --> 00:42:07.196 immersed, [LAUGHTER] that you just  don't see how much we think … 00:42:07.196 --> 00:42:07.520 LU: Yeah! 00:42:07.520 --> 00:42:11.520 HUIZINGA: … it's amazing. Well, I'm  just delighted to talk to you today,   00:42:11.520 --> 00:42:16.520 Shan. As we close … and you've sort  of just done a little vision casting,   00:42:16.520 --> 00:42:20.236 but let's take your daughter, my daughter,  [LAUGHTER] all of our daughters … 00:42:20.236 --> 00:42:20.600 LU: Yes! 00:42:20.600 --> 00:42:26.280 HUIZINGA: How does what we believe  about the future in terms of these   00:42:26.280 --> 00:42:32.920 things that we could accomplish influence  the work we do today as sort of a vision   00:42:32.920 --> 00:42:39.351 casting for the next “Shan Lu” who's  struggling in undergrad/grad school? 00:42:39.351 --> 00:42:44.480 LU: Yes, yes, yes. Oh, thank you for asking  that question. Yeah, I have to say, you know,   00:42:44.480 --> 00:42:49.480 I think we're in a very interesting  time, right, with all this AI thing. 00:42:49.480 --> 00:42:54.600 HUIZINGA: Isn’t that a curse in China?  “May you live in interesting times!” 00:42:54.600 --> 00:43:01.440 LU: And I think there were times, actually,  you know, before I myself fully embraced AI,   00:43:01.440 --> 00:43:06.880 I was … indeed I had my daughter in  mind. I was worried when she grows up,   00:43:06.880 --> 00:43:11.740 what would happen? There will be no job for  her because everything will be done by AI! 00:43:11.740 --> 00:43:12.580 HUIZINGA: Oh, interesting. 00:43:12.580 --> 00:43:17.640 LU: But then now, now that I have, you know,  kind of fully embraced AI myself, actually,   00:43:17.640 --> 00:43:21.640 I see this more and more positive.  Like you said, I remember, you know,   00:43:21.640 --> 00:43:27.920 those older days myself, right. That is really,  like, I have this struggle that I feel like I   00:43:27.920 --> 00:43:33.880 can do better. I feel like I have ideas to  contribute, but just for whatever reason,   00:43:33.880 --> 00:43:40.040 right, it took me forever to learn something  which I feel like it's a very mechanical thing,   00:43:40.040 --> 00:43:45.320 but it just takes me forever to learn, right.  And then now actually, I see this hope, right,   00:43:45.320 --> 00:43:53.480 with AI, you know, a lot of mechanical things that  can actually now be done in a much more automated   00:43:53.480 --> 00:44:00.720 way by AI, right. So then now truly, you know, my  daughter, many girls, many kids out there, right,   00:44:00.720 --> 00:44:06.880 whatever you know, they are good at, their  creativity, it'll be much easier, right, for   00:44:06.880 --> 00:44:13.080 them to contribute their creativity to whatever  discipline they are passionate about. Hopefully,   00:44:13.080 --> 00:44:18.120 they don't have to, you know, go through what  I went through, right, to finally be able to   00:44:18.120 --> 00:44:24.440 contribute. But then, of course, you know, at the  same time, I do feel this responsibility of me,   00:44:24.440 --> 00:44:33.240 my colleagues, MSR, we have the capability and  also the responsibility, right, of building AI   00:44:33.240 --> 00:44:41.880 tools in a responsible way so that it will be  used in a positive way by the next generation. 00:44:41.880 --> 00:44:47.440 HUIZINGA: Yeah. Shan Lu, thank  you so much for coming on the show   00:44:47.440 --> 00:44:53.060 today. [MUSIC] It's been absolutely delightful,  instructive, informative, wonderful. 00:44:53.060 --> 00:44:57.040 LU: Thank you. My pleasure. 00:44:57.040 --> 00:44:57.977 [MUSIC FADES]