In this episode, we talk with Leo de Moura, a principal researcher at Microsoft Research. We’ll dive into his work on Lean, how goals for Lean have evolved, and who can use it. We also discuss how Leo was able to implement such a system without being a programming languages expert
In this episode, we talk with Leo de Moura, a principal researcher at Microsoft Research. We’ll dive into his work on Lean, how goals for Lean have evolved, and who can use it. We also discuss how Leo was able to implement such a system without being a programming languages expert.
Watch all our episodes on the Building Better Systems youtube channel.
Joey Dodds: https://galois.com/team/joey-dodds/
Shpat Morina: https://galois.com/team/shpat-morina/
Leo de Moura: https://www.microsoft.com/en-us/research/people/leonardo/
Galois, Inc.: https://galois.com/
Contact us: podcast@galois.com
Intro (00:02):
Designing and manufacturing, installing and maintaining the high-speed electronic computer, the largest and most complex computers ever built.
Joey (00:21):
Hello, welcome to the building better systems podcast, where we explore tools and approaches that make you and us better programmers. I'm Joey Dodds,
Shpat (00:32):
Shpat Morina,
Joey (00:33):
Shpat, and I work at Galois
Shpat (00:36):
Galois is a research and development lab focused on hard problems on computer science. Um, today on the podcast, we're going to be talking to Leo de Moura. Leo is a senior principal researcher in the arise group at Microsoft research. He was one of the creators of the Z three theater improver, um, which is a widely known SMT solver used for tons of stuff like program verification, model checking, all varieties of automated reasoning. And most recently he's been working on lean, um, which is this mix between a functional programming language, um, and, um, uh, proof of system, um, that essentially makes it easy to write, correct. And maintainable code. So we're going to get into how lean came to be, what its uses are and who should be paying attention to it.
Joey (01:28):
Yeah. And Leo, it sounds like didn't know much about the core concepts of, of lean when he started. So we'll talk a bit about what it was like to dive into this problem. Not really, not really knowing so much about it. Um, and now that Lean's taken off, we're going to do a bit of a discussion about where it's being used. It's being used at Microsoft. Uh, we've used it at gala a bit and it's being used elsewhere as well. We've got the math community and the machine learning community, uh, pitching in and even, um, even, uh, just, you know, the regular old, uh, PL folks like us. And so, yeah, I, it's going to be a really exciting conversation.
Shpat (02:04):
Well, let's, let's listen in. All right. Thank you very much for joining us today, Leo,
Leo de Moura (02:11):
Thank you for inviting me to be here.
Joey (02:14):
So you've been spending the last, the last few years. I'm not sure exactly how many working on the lien proof assistant, although I'm not sure it started out being the Lean proof assistant. Uh, can you tell us a bit about that project?
Leo de Moura (02:27):
Yeah, we suffered the original goal was to have a library for connecting with systems like F star. Uh, Hawk is a bit one, so they to be you'd have more expressive watch rights. I mean, my previous CSUN was the trees for, for Southern logic, but you see sums, they all have part, you know, I have the beginning spikes and we watch provides better information for systems based on dependents type theory. Right. That's how it started. But, uh, depending types of really fun, quickly figure out we want to have our own brief assistance. And now became a programming language. We started was to have a library, became proof assistance to have a programming language.
Joey (03:22):
So there's all these tools, the tools you mentioned. Um, I think tools like, um, like I think you said Daphne, um, there's a lot of tools that basically call out to solvers. Um, these are tools that either our programming environments, um, or they talk about other programming languages and they try to do proofs about these programs. And it sounds like you're saying when lean started out, it was meant to be a library that sits between those tools and a solver like C3, basically.
Leo de Moura (03:54):
Yeah. We would probably implement some of the features we're having or customize them for the business type theory. But, uh, one goal was to avoid lost in translation problem that we have, whether we go from a system like F started has the business types and you have to go lower other logic. That's what C three supports. And the other goal was to try to buy destru Ward's rights for meters to improving interactive, to improving rights. We wanted to have a smooth transition between these two walls improvise. This is a solid library for systems like Dauphine that's urination of star Kwok is already benefits from automation like we providing C3.
Shpat (04:44):
So can I, um, uh, jump in maybe for folks, you know, when we were talking to, when we were preparing for this, um, uh, we talked about interactive theater improving, um, w how lean differs and just in general about maybe the value of proofs in general, uh, and, you know, getting the benefits of proofs by using a programming language like lean. Um, so maybe to step back for people who, who might not have those dots or connect those dots right now, um, what's interactive theater improvement, first of all. And then how does lean fit in with that, with that, or, or doesn't?
Leo de Moura (05:20):
Yeah, that's a great question. Not all interacting proofers are based on their rights, but they all, you can feel them like, uh, like some modeling language. You can have rights problems. You can precisely state a mathematical problem in your systems or software verification problem, right? Uh, and then you can interact with the system to construct approved property holds or the student's true rights. Uh, some, some simple proofs can deep prove they'll come magically, but in general design undecidable needs human guidance writes a difference from programming rights, such blame systems. What park, if start to see eventually wilds is like programming, right? And especially you are based on dependents type theory. Proofs are premiums rights, uh, approval by inductions. Like when you write a function by the cushion writes a fin to psychology, I think it's great. I mean, uh, even though sometimes I think it's great. It's for teaching people about proofs because they say, oh, it's just programming, right? If all of my teachers, sometimes they have gaps in their understanding what's approved is even, I met many top level mathematicians. They say, wow. After [inaudible], oh, now I understood the stuff I fought. I knew it, but I had only an approximation rights. I didn't really understand all did you pay,
Joey (06:58):
So to just lay out the landscape a little more, um, your history before you worked on lean, was working in [inaudible], which is an automated, um, I guess an automated tier improver, uh, you give it more or less the big math problems or big software verification problems. And it's sort of says, I'm going to just take what you gave me all at once. And I'm going to grind for, you know, maybe seconds, maybe a longer than the life of the universe. And eventually I'm going to give you back an answer. Yes. Um, and that was, eh, I think once you spend long enough with them, you, you start to learn, well, maybe this isn't going to solve all the problems I want to solve. And it sounds like you looked to dependent type theory as a way to maybe help people massage things a little more into let, um, let human step in and start to work on these goals maybe before Z 3d, uh, carried you across the finish line or something like that.
Leo de Moura (07:50):
Yeah, just with points. I think in our experience, the products that use the tree to find bugs were very successful. As a constraint solver, you have this big formline, you're trying to make it true, right? In a test kitchen, the racial problem, making true to finding boots for your program, that you exercise some behavior. If you are interested in, uh, we have many applications, the child will face successful Microsofts using this kind of application, right. Uh, where you're using the tree as a consultant sober, but using the tree as approver decidable, uh, first for finding bugs to find the [inaudible] rights into can always unfolds. You don't have to find inductively, variance, nothing like that. Right. It's really push a button this application. But when you're trying to prove the complexity keeps getting higher and higher, the system that's more and more unstable, right? So, I mean, we'll make a change, changing your problem.
Leo de Moura (08:57):
It fails to prove sometimes it succeeds. You'll make a tiny change. That is irrelevant from your point of view. But this is a system that's basis. All heuristics rights risks are going to fail you. We are not solving undecidable problems, right. Is just engineering or [inaudible] aspects of the stream. One aspect, you make three decision procedures, four classes of problems, right? You say, oh, this class is, decide what, which writes a very fishy procedure, but these are not the parts that you have to undecidable fragments. And it's based off your risk checks, black magic, lots of really scientific some arts rights.
Joey (09:39):
Yeah. And if, and if you saw me laughing there it's cause we, um, the team I work on has been spending our time trying to use C3 and its relatives as previous. So I'm sort of intimately familiar with, with the challenges you face there. Um, and then, yeah, and then lean was meant to isolate. Lean was, um, lean is, is a way out of this, this problem where, um, you know, instead of, instead of throwing things over the wall, basically saying, Hey, solver, figure this out for me. You, you get to do this guidance using programming as, as,
Shpat (10:12):
And if you, if you saw me laughing, it was because I did not understand 80% of them, No of this. Um, you know, I'm not joking, but that's, uh, I, I don't have my hands in this stuff day-to-day so of course I wouldn't, but, but in general, you know, this dark magic or whatever you called, it sounds about right. To me, whenever I try to kind of understand how some of these things work. So, so, but my, did I interrupt you joy? We're going to add,
Joey (10:40):
Oh no, I, I would, but I would say like in, in depth, um, you know, even though maybe you didn't understand a lot of what went by, it's worth, it's worth, you know, one of the things Leo is calling out is these tools feel like programming. So in a there's this crazy world of independently type programming and proof assistance where there's this deep type theory that goes into things. Um, and on the user end, w when things go, well, you don't have to worry about that stuff at all. Um, it it's, um, I remember a tool, the, uh, which is a tool like lean it being described as video game, like, and that you have this nice layout of the things, you know, and the thing you want to prove, and you just kind of take it one step at a time and figure out how to manipulate these things and massage these things, um, to eventually convince the computer that, that things are.
Joey (11:29):
Right. Um, so, you know, we have a lot of, uh, thanks to give to teams like Leo, um, Leo's team and the Coq team that, that take all this really hairy stuff. And at the end of the day, let you see this expression of I'm just writing. I'm just writing proofs, I'm just doing programming. So that wasn't really a question, but it was more, it was, uh, expressing a lot of gratefulness. Um, I'm curious, I wonder if we can even do, uh, a quick example of, of sort of what you, you know, uh, a vision of how lean might be used, um, by somebody who's interested in showing software correctness. So one of the goals that you really have for lean is that it's usable as a pro as a programming language, as a general purpose programming language. We started off talking about proofs and solvers, but lean really is turning into, or what lean is now. I think it's fair to say is a language that you can pick up and write a fast program in.
Leo de Moura (12:22):
Yeah, we wrote a lien, the new Orleans written the lien rights and the, our current school pilot link prover, it's all written in, uh, in scraped for us. I mean, we, our ministry prove the system a lot because the first one using users ourselves rights, eh, the other things that's, you see easier to make the, see some extensible rights, we'll have a lots of engagements for the community, the rights, many extensions, uh, and because you can use a to extent leads itself, uh, you can move different directions, rights, uh, quite diverse, have users that have mathematicians, pure mathematicians and have users such as computer scientists rights. And they have completely different ideas of what links should be. But if you make accessible systems, they can customize themselves in. They do. It's quite funny.
Joey (13:26):
So lean itself is, is evidence. I'd say that lean can be used for the computer scientist types. Um, but there's also been a really, uh, very large amount of interest from the mathematical community. And this is people doing real analysis and things like that, right?
Leo de Moura (13:44):
Yeah. Th there's a few months magicians applied. Uh, I have sometimes a hard time communicating with them. There's a mismatch in our languages, uh, but it's great. Uh, it's great to have users definitely for a new language
Joey (14:07):
And it's, it's great to build a language that can be what be, what you want it to be in a sense. Um, it's not, it's not easy to support both of these groups, but it sounds like a path forward. Is this extensive?
Leo de Moura (14:19):
Oh yeah, yeah, yeah. Yes, yes. That was one of the main motivations. I mean, Sebastian Orrick and I, uh, when we started designing for one of the big motivations to make extensible, because we know people wants to move things in different directions. Uh, everybody has a difference it off what's discussed structure. Do they came to stone mines now for their home needs, right? Uh, yeah. Yeah. It's quite different. So, uh, also for us as scientists, because we have been programming rights for a long time, they must magicians are like, they're just now using something shoes for all languages rights we have been using for ages now, rice, the sciences, uh, for the edit for the languages, a formal language rights. And you have can using where users, we learn that lots rights. Uh, if you go back into the past, people would be talking about all let's use flow. Like nobody uses stuff anymore for teaching or spec-ing program rights, putting the best people. This was an amazing idea or using natural language. Right. So let's create a programming language you're writing in English. Right. It's a horrible idea. Right. So we less a hard boys. Yeah. Uh, but people are trying to do things like that and scrapes extently this direction. If they, once they'd be there will succeed. Right. I mean, we failed the sculpted, the scientists straight creates a language it's looks like English rights. Uh, but maybe they won't succeed.
Joey (16:06):
Yeah. It's not so much a horrible idea than it is an impossibly hard to achieve idea. Right. It's on paper. It seems great. And the outcome would be wonderful, but, um, that's a, it's definitely a harder thing than it seems to accomplish some of these things.
Shpat (16:21):
Yeah. And so my understanding is that some of the, essentially some of the topics and some of the core concepts that ended up being implemented in lean were new to you. I think even something is core to it as dependent type theory. Um, is that true? And I'd be curious to kind of hear what held would that learning? How, how did you get yourself up to speed? Because I would imagine that there's some people listening that are in the same position and not only did you get yourself up to speed, but then you implement a language that's proven to be very useful to.
Leo de Moura (16:53):
Yeah. I just have any backgrounds. Uh, it's actually a blessing because you don't know how hard the problem is. Right. So you've given us is great. If you do, can you say, oh, I'll just shoot a lot to be hard. I can do it to staff because you aren't aware of how complicated things are. Right. Uh, but I, I, it's great to have, I have many colleagues of mine, uh, uh, joy mention F star and cue helped me adjustments here. It wasn't Microsoft. He was our user rights. Uh, he helped me a lot. Uh, Jeremy Africa, arts, uh, he was an expert in Isabel roof assistance. Uh, he gives me lots of feedback. Uh, he also was pretty good user of rocketry. I mean, he was amazing. He's a bell pre-boot caulk. He could also balance the difference between the different species is a bill at the time. Uh, I wouldn't be assessed culture rule also helped lots. A small few may have met him. Uh, yeah. Having colleagues helps a lot.
Shpat (18:09):
I was going to say mostly through people you got.
Leo de Moura (18:14):
Yeah, yeah, yeah. They spent hours talking to me. Yeah. It's great. To me, it was basically [inaudible] was written by Andre power. He has a blog, he has small, tiny type checker for the business. Like theory I've been was one of the first things I do. Okay. Let's follow his tutorial. Let's implement this stuff. He has the year.
Joey (18:50):
And I guess, yeah. To give a shout out to the field community like this is, you know, if Leo comes knocking, maybe a lot of people will talk to them, but I don't think given most of the people you described, I don't think that was special treatment for you. I think that this is mostly a group of people that, um, are really engaged with the student community and helping anybody that wants to learn. Um, so I, I, this is, this is something that's not, you know, that that can be achieved if you want to learn. And if you have specific questions, um, definitely start with the tutorial. But most of the people that you mentioned there are pretty open to collaboration and to helping to helping everybody learn.
Leo de Moura (19:27):
Yeah. Lots very, I was face to face and all these examples I gave you. Uh, but some of them are very active online for engaged with him when you answer your questions. But I don't use these kinds of tweets. I don't even have, I have a Twitter account. I never use it. But, uh, yeah, I'm too old for this kind of technology.
Joey (19:53):
You are on the, um, you're on the lien Zula if I believe. So there is a way to engage with us around lean if somebody is interested in,
Leo de Moura (20:01):
Oh, yes I am. But I have hot time for just stuff. Uh, I find it super distracting. Uh, yeah. I don't know. I, I mean, uh, [inaudible] much younger than he was with this book here. He has a screen zipped the messages there. He stops answers. Something goes back. Could she use to program? I can do that. And I need full concentration. I can keep switching between text messages. [inaudible]
Shpat (20:38):
I, you know, I don't know about young and old. I've seen that fall all over the place, but it's arguable, which one is better or more, more productive, you know, some would be on your campus squarely. Yeah.
Joey (20:52):
Yeah. I, it sounds like, and I think this is honestly worth diving into, cause I, I would view as a very productive person and I don't think there's a lot of debate there. Um, it sounds like, you know, who
Shpat (21:03):
We should, we should chat about. We should chat about that after the,
Joey (21:08):
Um, lean is a, is a huge accomplishment. Right. And I don't, again, like, I don't think anybody would, would look back and say like, yeah, I could have done it. I could have done it in half the time. Right. Like Leo is obviously spending way too much time on Twitter or, you know, anything like that. But it sounds like you know who you are and how you work well. Um, and I, as like, I, I mean, I don't want to like ask for the secret to success, but, um, how do you, how do you work so well,
Leo de Moura (21:30):
Well, do it fail again? Fail again, fail, right? I mean, people don't, some people may not know, but before I wasn't Sri with more yikes before that was nice. Yes. Uh, with Harold, I mean, we try, uh, we just worked so well. [inaudible] the first submission was crap. The second one was the second one we wrote that's 1.0 0.1 or scrap the [inaudible] we wrote, they assess working with Microsoft. We wrote the first tree was so, so the second one was much better. The third one even better and keeps improving by same thing for me. The first one wasn't usable. The second one, what SIM you managed to use, but it was horrible. The community growing and now we're super hopeful. That's the way more successful than normal person is night and day the experience.
Joey (22:47):
So there's, I mean, this sounds really hard to like it wasn't, none of the earlier liens were a small amount of work. And I mean, some of them were fully like lean three I've used, and it's a fully usable, interactive proof assistant, but you, you made the call to, to throw it out and start fresh. I think obviously you have a lot of experience that spoke to that and made it clear to you that that was the right thing to do. But are you, how confident are you when you make these calls to, to start fresh?
Leo de Moura (23:14):
It has sometimes again, Ziegler, right? I mean, if you can do the programming language complicated, I never wrote a program approval system. When we say programming language, that's the rates efficient codes. Right. I, again, and we fought, oh, we can do it smart. That's hard we can do. It was basically Sebastian writes was together we're together and see, and he said, yeah, let's do it. So me doing it was way harder than we expected. Again, colleagues helped a lot. Simon Peyton Jones helped a lot. So give you feedback, explaining things that we had to do to achieve good performance. Right.
Shpat (24:03):
So there's, there's um, I'm not going to call it ignorance. I'm going to call it optimism and maybe naivete at the beginning To get started. Right. Like doing, doing version two and three and four and sticking there, there must be in addition to that, something else That helps. It's probably, you know, the way joy, I've never actually heard anybody. Um, describe or any, any of these, you know, like you did, you know, it's a little bit of like a game and it actually made a lot of sense to me after I haven't seen people do that. I wonder if there's part of that too. I mean, it's a sort of fun, you know, there's a reason that people like Minecraft you're, you're slowly building things and doing them. Right. And sometimes you fail.
Leo de Moura (24:52):
Yeah. Yeah. I've seen many people claiming that it's protective, disprove assistance stuff. It's just like a puzzle rights for solving a puzzle. Uh, you can easily spend a lot of time doing it. Sometimes I test you say [inaudible] meaning just to see, we have lots of experience using mini as a programming language, but we don't spend a lot of time proving things using the system. But sometimes we do it just to pass how comfortable it is, what are the pain points? And you can easily spend a lots of times gets into this stuff. In this one thing that's quite different from programming is that the pharmacist writes checks to women. Our rights can program your type check. Yeah. I mean, from such the performance, you have to factor or assign this kind of thing. Doesn't happen when you're just proving rights.
Joey (26:05):
It's a, when you're writing proofs about programs and I assume it goes for Matthew in this w this very rare situation where you know it, you know, what the outcome looks like, and you just need to get there. And then when you're done, the computer tells you you're done. And that's a pretty, it's a pretty rare feeling and programming to just like, have someone to say, yeah, you did it. It's right. Like, you know, back it up because you know, for anybody that's spent time writing software, there's always this. And I'm sure for you on, on the developing lean side all the time, there's this nagging. Well, what if I got, what if I got something wrong? What if there's a bug that I, that I haven't caught yet? What if I missed a site of usability? Um, there's so many lingering questions all the time, but inside of the proof world, you have this certainty. That's a really, really nice place to live. Sometimes
Leo de Moura (26:53):
That's one thing that's really hard. I found really hard. Any programming language with respect to the tree, it has a clear InSpec rights has the specification, what you should do, right? So you have a well-defined in the language as inputs, and it should be true. If the problem is all satisfiable or false, the pencil, how you decide you would just have to return that to possible. It's not satisfiable or is such fiber in Houston. This formula, right? The spec is very, well-defined this right. There's value for misunderstandings.
Joey (27:41):
So it's, uh, it's it's you give me a, you give me a formula. I'll tell you, uh, I'll I'll tell you true or false, more or less. It's a little more complicated than that, but it's this, and you fully described the way that the formula can be written in the first place as well. And very simple terms,
Leo de Moura (27:58):
Uh, just sparked you can focus on your, all the performance procedures of the frankness at decidable, but this is insane. So like a programming language there's locally, a spec on the language should be, which features should be bare. For instance, you ads does interactive tactics. That's how you build proofs. Interactively people have different ideas on how things should walk using a what should do. He wants that to behave that's way, use B once the opposites. And once he came after, it was really hard for me to learn that you can't make everybody happy. Right? I mean, we've seen stories to make everybody happy, but Lee or any other programming language, it's really tough language design. The last one is really tough.
Joey (28:57):
But through all that, you, I get the sense you want users. I feel like you want people to use lean. So it hasn't, it hasn't, it hasn't scared you off.
Leo de Moura (29:07):
Um, no. Yeah, yeah, yeah. Uh, so some users, I found that I think my experience is much easier to interact because they know they have, they know how complicated things are. They have a better understanding or more realistic expecting. They have users, many programming languages before I, especially, uh, for me languages, that's, uh, all research from his social labs. Why they're not as polished as a programming language that's used in industry. Right. Versus I remember colleague of mine saying, well, I have to send out compiler. Uh, I mean, usually it's a new one. If he tells me they have always here, that's all I want. I don't want a nice phone message once anything, just tell me where it says more or less. I mean, seven rounds here. That's the expectation, right? If you're using something like TypeScript, your expectations are much higher, right? It's once or Russ, Russ is amazing. They are messages. They produce so lots of engineering care rights, but you need a big team of lots of people to do that. When you're starting a new programming language messages, I use usually crap. Right.
Joey (30:29):
And it's not, it's not easy. It's, it's, um, there's deep scientific questions basically. And how do I get good air messages? It's not like you just like, oh, like you didn't write a very good description of what went wrong. And I'm sure one of the things you've iteratively improved is, um, figuring out how to track things better as, as sort of as information moves through the language. But this is not a, this is not an easy problem. So, you know, definitely like loads of credit to languages like rust and TypeScript and, and half how much work and how deep of an understanding of the language those engineering teams had to have to make that stuff work. But it sounds like you want to make lean into a language that's as usable as rust or TypeScript, is that it, is that an ideal end goal for you? Um, w we can talk about whether that's accomplishable.
Leo de Moura (31:16):
Well, we can say it's a drain, right? So to me, I think both Sebastian and I would be extremely happy if we have something as user friendly, as rust rights. Uh, and also if you want, it's impossible for two people to build something like Russ, you need, uh, engagements from the community. And the way to get to engagements is to start to making something that's seems path, right? It's, uh, let's can be extended so people can work in different modules. Uh, freezes for mine off mine from Microsoft is helping Danny Fabion. It's great. We need more people like him with outsides, if you want to be as big, as far as risk has a lot of people help.
Shpat (32:09):
The starting point, there is just starting to use the language for something. Um, and if that's the case, um, if people are listening and wondering, well, I guess the question is who, who should consider just jumping into lean right now? Lean forest,
Leo de Moura (32:24):
Uh, people that's life. Well, the first thing I think, people that are excited about the programming languages, one to learn dependence types of benefits right now using four, they can have a lot of fun. Uh, I think right now is if you have, like, your interest is in informal mathematics or proven verification or proof assistance, you could benefit. But if you are a programmer, I think right now the main benefits is if you want to, other than stack theory, you feel excited about his ideas. I think [inaudible] language,
Joey (33:00):
But what I'm hearing there is you don't already need to know dependent types. Lean would be a nice way to, to, to start basically, and to interacting with the lean community.
Leo de Moura (33:10):
Yes, yes, yes. But, uh, I F I think I have a bias towards the tenants types, because I think it's really beautiful. I mean, uh, for me, I, I was so excited when I started learning, see things, I think many of your listeners, if they're subtle, I mean, they will also be super excited.
Shpat (33:30):
I think I'm going to finally go and check that tutorial. Imagine that for this.
Joey (33:34):
Yeah. It's uh, yeah. And I don't, I don't think, I think the, even starting to dip into what dependent types is, is going to be too much of a diversion, unfortunately, but yeah, I rec I agree completely. Um, and, and I mean, the most basic lean programs you don't need dependent, you can sort of, you can start programming and, and learn as you see the need, basically, which I think is a really ideal way to, to introduce people to new topics is to say, well, like you program, and maybe you sort of see this thing that you wish you could do, and you ask, how do I do this? And you go to the, the, the, you know, the Zula chat, for example, I've found to be a great place to interact with a lot of people who are really eager to help. And you say, how do I do this?
Joey (34:12):
And then all of a sudden they introduced this concept and you say, okay, well, I, I really care about this. Cause I was already trying to do the thing at accomplishes. And all of a sudden you've started learning, you know, you've, you've taken your first step. I, I find that approach can be so much more effective than like I'm going to crack open the book on dependent types and just start on page one. Um, as soon as people can dive in, usually, um, they, it can be really helpful to just understand why, um, rather than just learning for the sake of like,
Shpat (34:41):
Well with that. And for me, at least I think, well, the, the, the project or what they're using it for, even if it's, you know, primarily for learning, um, what sort of, uh, types of projects do lend themselves better to, to doing this, um, uh, or what sort of little toy examples or burst something larger. Um, I wonder if you have any thoughts on that,
Leo de Moura (35:05):
The things that would be really my smell, if people want to write extensions, right? That's one thing that's, uh, would be super exciting. People [inaudible] extent, leads self, I think can be done now would be super useful for the community rice. There are other projects like it's Gamal, I mean, Joe Hendrix had this demo of the robots that was super cool, right? Ish, he's basically controlling or robots using lean rights. Uh, it has a blog post now, a super exciting projects, right? So Lee is the face of C, right? Since we projects that you need to call the [inaudible], that you have written a different programming language, it's kind of project east possible right now. Right. I can tell you about projects. We have it's Microsoft that you're using, for instance, uh, they'll sell some, has a precious called the IMO grand challenge. The goal is to get to the goals and national mathematical needs.
Leo de Moura (36:13):
Yeah. Right. Uh, and for [inaudible] for high school shooters for the problems are really tough. I think I would get a zero. If I tried to compete, you'll have to train for these kinds of stuff. Right. Then bunch of streaks. And if they weren't there today, I guess zero rights, one, uh, I guess one problem. Uh, but he was right. I see somebody that can solve these problems automatically. And one set, you have to write custom domain specific information, right. That many techniques, uh, that you can, they are not general bubbles that face specific to a class of problems and he's doing this stuff using me. Right. Uh, another thing that's, uh, we're excited about is using, using the crews, optimizing patients' rights, you have a machine learning is a big topic now, uh, in rights to computation, that's abstract, these a bunch of matrix multiplications rice in the one shoe optimize this kind of program, right. Proofs might help, uh, that's one kind of project project that's really excited about
Shpat (37:33):
For my learning on that one. Um, what makes the way lean does things more, just better for those sorts of optimizations?
Leo de Moura (37:42):
Oh, because you can, uh, you can, you can not just write computations, but you can write skinny link programs. This manipulate show programs, that's the form of the test, right? So you can write senior living, approve them. That's treats your program that she wants to my SIS data rights, your rights have net approving that's treats, Jolene prelims this data and tries to optimize it. He may try to do like a such of over the space of possible personalization and fight and optimization that you would never think of. Or would it be too time-consuming each writes by hints writes that that's the kind of possibility that's attractive. Right. So rights programs that such this space of solutions, rights, the space of programs.
Shpat (38:36):
That's amazing. Yeah. I would love, frankly. I think, I don't know. Maybe it's just me, but like having a very simplistic tutorial that walks through an example like that, especially as you said, you know, machine learning is, you know, is in the news, but, uh, it will be very interesting.
Leo de Moura (38:58):
Yeah.
Shpat (39:01):
Did you have any other examples that you wanted to walk through?
Leo de Moura (39:03):
Let's see.
Shpat (39:05):
We don't, we don't have to. I just wanted to make sure I didn't interrupt you.
Leo de Moura (39:08):
No, no. I just want the main true examples. The true application sets for considering Microsoft. Uh, but in the math conducive, they have many rights. I mean, if you go to the channel, now they have this condensate and mathematics channel, a sub channel there and the need for a channel. Uh, and they're trying to finalize this results for, for this famous mathematician, uh, pick the shows is his name. Uh, and they are super active. Uh, yeah, math. I don't go there. I don't even understand what they are doing. I mean, tell me, they tried to explain to me why does this relevance? I don't get it, but I trust that they know better. Right. So they probably, they told me that's really important, but I don't really understand the math,
Shpat (40:06):
If they're doing very important things and you're working on the language and the tools must be a little pressure to,
Leo de Moura (40:12):
Well, for sure. Sure, sure. Yeah. Uh, yeah,
Joey (40:20):
So we're running a little low on time, but I wanted to ask a final question, which is, what do you view the most successful version of lean as being, where do you want it? Where do you want lean to go? I've heard that maybe you're thinking about integrating lean with, with rest of it. Yeah.
Leo de Moura (40:37):
Um, we want to have, uh, a programming language that you can generate sufficient. Kohl's right. I mean, it's high level, but you can use the proof's it's efficient codes, uh, support for metal programming rights or human rights programs. That's lights. Uh, you can prove small properties. I'm ultra-premium was big properties is drug decision, but you have support. You have this option. If you want you to have integration, this is user experience for systems where a system like Russ provides. Uh that's for sure. It's one of our goals. You mentioned integration for us. Yes. We definitely want you to do that. So I think it's very compatible through us is a pure functional programming language, but it doesn't use a generational or tracing collector. Uh, it's just it's uses reference. Counting is very compatible with the risk system. Right? Well, if our goal is to have a wage of whole risk functions, that's focus written in breasts.
Leo de Moura (41:49):
That is really confidence for the user, right? So you want to call some risk function. It should be super easy to do. That's one of our dreams to have this kind of capability. Uh, what, why do we want that? Because Russ is getting really big, many libraries. So you could use all the libraries, they have development rights. That's what was motivation. It's easy to use. I don't know if you have users rests, but the package package manager, who's awesome. Have them be sure to have a package manager like cargo rights, uh, being integrated greats rights, because if you could use the fuel like that, uh, Russ allows you to achieve see performance now, right? But most of your proves don't need to achieve see performance. It leads, which is extra program than breasts, right? Uh, it's much higher levels like the feeling for if people are familiar with Haskell Ling has school vibe rights. When you're programming, you have, uh, all these goodies that you have in your high school, that's probably way more flexible than the rest, but Russ has the core performance rights you can achieve really high high-performance with rust. And I excite a combination is, okay, you need extreme high-performers who writes breasts, who can integrate smoothly, that rests rights, rights, then it's you want to show us some parts of the culture racing, meaning, prove it's correct, mean rights. Uh, I, I think some nice, uh, would be a nice experience to users, right?
Joey (43:33):
So it sounds like everything just there's the vision where everything works nicely between the two languages. And maybe I do just a package import and maybe know that it came from rust or lean, but I don't have to worry about it so much as it just works well with whichever type system, um, I'm using it. It seems like it would make a lot of sense for the rest community where there's clearly a huge appetite for
Leo de Moura (43:57):
Yeah. It was user excited about then a C user rights rust is already so red to using a functional, like functional, like concepts. You have lumped with those who have all the staff lats and so on. It's much closer to choosing the right.
Joey (44:21):
So if you're, if you're a rusty user, who's looking to take correctness a little farther. Maybe, maybe you are an ideal early adopter for
Leo de Moura (44:29):
Sure. Ilene came from breasts. Yeah. We'd find someone to watch as a singular freezers. We have latch rests for mutual variables. We have. Nice.
Joey (44:47):
Yeah. So you'll be able to carry across some of the things you've, you've learned from rust and make use of those directly
Leo de Moura (44:52):
In LinkedIn. For sure. That's excellent.
Joey (44:55):
Well, I think that's about all the time we have, uh,
Leo de Moura (44:58):
Much for joining us, Leah. Yeah. Well, super fun. Thanks for the invitation. It was my first podcast and it was super fun. Ours too.
Shpat (45:07):
Yeah. You couldn't tell It was, it was, it was a lot of fun talking with you, Leo. Thank
Leo de Moura (45:16):
You. Thank you. Thanks so much guys. All right.
Shpat (45:20):
This is another episode of building better systems. Join us again. Next time.