Can We Trust AI-Written Code? Why Executable Specs Are the Future of Software ft. Gabriela Moreira

Speaker A: I think some software will fall into those categories and then there will be more, like business people with no technical expertise writing some software. And in some cases that will be fine. And there's like another category where, like, correctness is super important and if you don't do things properly, people will get hurt, money will be lost, a bunch of problems will happen. I think there's less of a chance in some of that that we can ignore code completely or ignore how the systems behave and just trust that AI will do the right thing.

Speaker B: Foreign. And welcome to, uh, colors of Web3 and entrepreneurship. My name is Lum, your Web3 and entrepreneurship host. For those of you who are new to the Show, Colors of Web 3 and Entrepreneurship is a show highlighting the journeys of builders and innovators in Web3 and entrepreneurship. Some topics expected in Web3 may get technical, but we do our best to keep it accessible for most of you. If you am today, we are on episode 89 today, and here today I'm joined by Gabriella Morena. She's the CEO of Quint Company. Yeah, Gabriela, could you give a quick introduction by yourself?

Speaker A: Yeah, thanks for having me, Lum. Yes. So I'm M. Gabriela. I'm CEO of Quint, as you said, and I have been. I fell in love with programming over 10 years ago and I really liked what it does to my brain. And then over my university history, I fall in love also with formal methods. And then I really like what that does to my brain. Uh, I really like how we can think about stuff and I want to bring that feeling, uh, to everyone, what it can do to our brain when we have confidence, when we build software with confidence, and how more reliable the results are when we are thinking about things. And especially with AI, I don't want us to lose that because, uh, I think it's very fun and a very important thing. So, yeah, that's me.

Speaker B: Um, I'm sure many of you will be interested in knowing about what you did in the past, maybe about your professional background leading up to the current day. So feel free to pick a point in time, maybe after you graduate from college or something, and then walk us forward chronologically. Yes, so we know more.

Speaker A: Yes, let's see. Uh, so at university I started doing research, uh, with compilers, and I really like type systems. And then when I was having to do my bachelor thesis, you have to pick a theme. And then I was introduced to tla, which is a formal methods language and I really like it. I was super excited. So I started building tooling for tla. And at that time I was also working in the industry, uh, working with like, event driven systems, distributed systems. And I realized how hard it is to come to think about all of the possible scenarios, like, super complicated. And I was like, yes, this thing that they are building, like with TLA would really help here. But then I was trying to get us to use that, but it was very difficult to justify, um, at that point. So I was building my. I was writing my bachelor thesis about this and I was writing my master thesis about this. Uh, and I was presenting, um, my work at a conference. And then Informal Systems, uh, the company I worked for, uh, found me there and they were also doing similar things for tla. So they, uh, invited me, uh, to work at Informal Systems. And, uh, then I've been building. So we started building Quint back then and. Yeah, that's how I ended up here.

Speaker B: Nice. Wow. Interesting. So would you say you have more like a research background? Right. And then somehow.

Speaker A: Yeah, it's a very. I think it's a very balanced mix. Uh, so I had a few years in the industry before I joined, uh, Informal Systems. And I also had. I have an academical background, but I don't have like all the way to a PhD. I just did like a bachelor's and a master's. I also, uh, forgot to say this, but I was also teaching formal methods at the university for three semesters. So I also had that. I really like the university. I think, like when I go back there, it's, uh, very valuable.

Speaker B: Nice. Awesome. Yeah. Could you give a quick, simple introduction on what formal methods, Formal system is about? I'm pretty sure that most of the viewers are probably not like mathematics majors. Right. So they may not be so much. Yeah.

Speaker A: Uh, so formal methods is a field where you are trying to show the correctness of your software. So you usually have a different sort of language where you specify what you want your software to do, how it should behave. And it's not only for software. Uh, I, I'm obsessed with software, but it's also, it can also be worked just for hardware and even like for everything. But it's mostly software and hardware. So you are, you specify what it should do and then you use these tools to prove mathematically that it actually does what you said it does. And, uh, there's different levels, so you can go all the way to like, mathematical proofs or you can have like something close to that. Um, so there's some different levels of verification. Can also try to. There's, uh, Also a ways in you can run verification on your code when there's a lot of constraints. So the further you closer you are to mathematics, then the stronger proofs you can have and the strongest things you can do. And then the closer you are to code, uh, there, there are more constraints, but still like there's this whole field of things you can do.

Speaker B: Nice. Wow. Yeah. So, yeah, I'm curious. I mean, I actually was a mathematics major. I also learned a lot of like CS back in the days as well. And even now. Right. I think a lot of you were just like self taught. I'm also one of those SEL taught as well. Um, could you share like some ways that people or company using this in like real life formal method?

Speaker A: Yeah, Uh, I think the nicest case I can talk about is, uh, from aws. So aws, I guess everyone informal methods quotes them because they have used TLA extensively and they have been publicly reporting what they did. So they, they have a couple of papers where they explained really well how they took advantage of tla and um, it enabled them to find bugs in software and also. But not only find bugs, we're able to use TLA for design in a way where they can also do, uh, aggressive optimizations on software. Because you see if you model something, how it behaves and then you verify things there and like, okay, this works. Now what if I change this a bit and optimize it a bit, does it still satisfy all of those properties? And if it does, then you can go now and make that optimization in code. Uh, so it superpowered them, um, into doing some cool stuff. So I think AWS is like my favorite use case on the whole industry. But there's definitely more of them.

Speaker B: That makes sense. Yeah. And I mean, AWS is now the huge behemoth that everybody probably knows about for sure. Cool. Um, yeah, I'm curious. How did you learn about AI in the first place? What was your first introduction to AI? Was it in college or was it after college?

Speaker A: Yeah, it was definitely after. Okay, So a general AI. If you're not talking about LLMs. I did have AI classes in college.

Speaker B: Traditional ML is fine.

Speaker A: Yeah. Okay. Traditional ML. Yeah, so, yeah, so that was in college. And also I had, even before I had the AI chair in college, uh, in university. Sorry, College and university are interchangeable for me because in Brazil there's.

Speaker B: Yeah, yeah.

Speaker A: So in university I had the, uh, uh, AI chair. And before that I was actually, I started my internship in my first job and there they put me on the data Science team. It was kind of funny because I joined the internships. Like they got, they saw me on university, wanted to hire me. I was not very interested in started working back then, honestly, I was very in my academical work. But they kind of convinced me, no, we are a cool company, join us. Uh, and I'm like, okay, let's do that. And then I joined the company and I was not sure what I was going to do. And they were like, you can be either a software engineer or a data scientist, uh, for internship. And I'm like, science, this sounds better. Uh, let's do the data science thingy. So I ended up doing like six months of data science and I learned a bunch of about machine learning and stuff. But uh, I didn't really enjoy it a lot. So I ended up switching to the software engineer career path later. So when I got AI, uh, in university, I already was familiar with all of the concepts and stuff.

Speaker B: Interesting. Yeah, I think that's interesting that he didn't really like data science. Data science. I think that point was renowned to be like, what, the sexiest job of the 21st century at some point. I think in Tama. Yeah. That's fascinating.

Speaker A: Yeah, I think it's fun. It's very respectful for profession. I just, I, for me was not like tickling the right parts of my brain.

Speaker B: I see.

Speaker A: Had fun. I had some cool dashboards and analyzed some like health data from my city. Uh, it was fun, but not my favorite. I got more fun in the software engineering world. Yeah.

Speaker B: Oh, good. Yeah, I think for each person have their own thing. For me, I like building everything, so I like learning a bit about different fields of software engineering and data science. Yeah. Before we deep dive into the current company, Quinn, could you maybe share with us a fun question? What do you do in your free time when you're not working with computers and math and AI?

Speaker A: Yeah. Uh, so my default question for this is just I play games. That's still true, but less and less I can find time to play games. So I'm not sure how much of that holds still. But yeah, uh, I do now I'm mostly more chill and just watch some Netflix or something, hang, uh, out with some friends. And I like to play also board games. So all of that stuff. I still do play games from time to time. Yeah. So it's just not so much free time as I used to have. Yeah.

Speaker B: What is your favorite game? Favorite game? Game console or game console or game console?

Speaker A: Yeah, no, the PC. I'm a PC gamer. Favorite game you can have the whole podcast about this. I was a really big fan of Borderlands 2, so potentially that one. I can list that one.

Speaker B: Nice. Nice. Yeah, I think I kind of quit playing games a very long time ago, but I think my childhood was at many years I played different games like RPG and strategy and whatnot. Uh, it was certainly a very fun time of my life, for sure. Cool. So, yeah, without further ado, let's uh, go ahead and deep dive into your current company, uh, Quint Company, Right. Where you are serving as the CEO at the moment. Yeah. Maybe if you could share a little bit of, um, maybe a little bit of background of how the company kind of begin, uh, maybe the history of it. And then if you have any presentation material to share or demo to share with people, I think to make it more accessible, feel free to share that as well.

Speaker A: Okay. Yeah. So let's begin. I already said TLA too many times on this podcast, but I'll say a few more. So TLA is a formal specification language. And as I said, like, I was working with that in my academic life and Informal Systems. So Informal Systems is where Quint was born. And then now we are spinning out the new Quint company. So just uh, that for that context. So at Informal Systems, they were also doing some stuff with TLA because, uh, Informal Systems is a company, uh, born from the Web3 world. And uh, there was a bunch of demand for like this correctness, um, guarantees. And uh, they were building consensus algorithms when they wanted to make sure the consensus algorithms are correct. So they were, um, writing TLA specifications and trying to generate testing out of tla. And it's very evident, uh, if anyone looks at TLA from a programming background, it's very evident that it is difficult to understand what's going on. And it's. Even if one person goes and like breaks the difficulty entry bar and learns it, it's hard to like, okay, now let me teach my colleagues to also do this so we can leverage this as a team. So Informal Systems was struggling with this, so getting tla. They appreciated the value out of tla, but they were struggling with getting more people to start using it, more people to read it and understand the definitions. And they, uh, realized it's just a syntax problem. The syntax is too complicated. So maybe what if we just build a new syntax so all of the same tooling, but just a new syntax. And that's where Quint was born. So Quint was just like a new syntax for tla. Everything else was amazing. But then we Started tackling other problems on tla, right? So one of them was like, the people were like, okay, I wrote my specification. How do I run this specification? No, you don't run it. You are going to verify it. But the person's like, I don't want to verify it yet. It's a first one to run it. And there was no really, like a way, an obvious way to do that. And in Quint, we made it very obvious. You have Quint run command, so you run it, um, and you see what's going on. So we started addressing more of these problems and then this. We wrote the simulator in order for you to run it. It's just, it runs a simulator of your specification. And this simulator becomes so much valuable to us, us, because it allows us not only to do the verification later with the existing tools, but with the simulator, we can now actually iterate faster and understand what's going on. So the simulator became the most valuable thing for us. Um, but it was still very hard, um, to justify that. Even if the value was amazing, you still had a great cost because you have to write all of the specification for your system in order to get that value. So, so writing that specification, learning a new language, it takes some time, takes some effort. And then AI came and LLMs came and now suddenly, uh, learning a new language is not really a problem. You can just get AI to write that for you and then you don't have. The cost of writing specification is so much lower now. And so we're like, okay, finally we can have people, uh, get this value without so much cost. But that's not only it, because now there is also a bigger need for confidence. So it's like a, uh, perfect fit. And that's why we are now spinning out queens, because you can make a product out of it, not just have this internal research thing that we are super fan of, but we didn't know how to make it feasible for everyone to use. Now we have that. So that's why we decided to make

Speaker B: a company that makes sense. Yeah, I think that's pretty cool. Yeah. Can you walk us more into details? Feel free to share any presentation or, uh, slides that you might have as well about Quint and what the new company will be about.

Speaker A: Yeah. Yes. Let me share then, just to give you more of a sense of.

Speaker B: Sorry.

Speaker A: Let me click the button for sharing.

Speaker B: Sure, sure.

Speaker A: Is here. Okay, There we go. Uh, so this is our website. Uh, and yeah, so there's some comparison here with like, what, uh, people. Then this is actually this, this website is a bit like it's done before, even the, all, all the LLM stuff. And we probably will update it with more like uh, how it fits into the AI story. Um, but still, this is what we had for years here. English and Markdown are not good ways of writing specifications. They are not checked, they are not executable. You cannot ask questions or get understanding out of it. The best you can do with English in Markdown is read it or ask AI to read it if you will. Uh, but you cannot um, get much understanding out of just English in Markdown. With Quint you can. So Quint, first of all, all of the stuff you define in English and Markdown can be checked, type check, but the main point is that it can be executable. So instead of having this like English document, you have sort of like the same level of like uh, a high level document. It's not going into implementation details. You have a high level description of your system that you can execute and then they can see behaviors, you can see how it behaves and you can understand what happens. And you can also define um, properties and things about the correctness of that. Uh, and this doesn't have to be like super complicated mathematical stuff. Just like what are your requirements? What do you want to hold? Um, so I just want to mention mostly this comparison to English and Markdown. And then there is this, um, in AI there is a spec driven development conversation. Uh, so, uh, there was ah, uh, a talk in the AI Native conference, I think like one and a half years ago or something, maybe one year ago. And they were like, oh, spec driven development is the future. And I was like, yes, finally people were seeing it. And then they were like, specifications are English and Markdown. And I'm like no, no, no, no, no, no, please come back. That's like it is the future. Like it makes a lot of sense if AI is generating all the code and the focus is on the spec. But how come we are using like just English for the spec? It's like we're losing everything that we like in programming. We're losing the ability to run and interact with things. Right. So we really expect driven development needs to be done with execution executable specs. Like that's one of the main points here. Um, and what I want to show maybe.

Speaker B: Interesting. Yeah. So the language probably has its own syntax and the way it's written. Is that correct?

Speaker A: Yes, yes, that's what I was thinking to show next. Maybe, uh, let me see if this is big enough. Um, so this is a very quick, um, explanation of model checking, which is a field of form of verification where you start, like you give, uh, you start with a model what your system does and the properties you want to hold. You give that to either a model checker or simulator and they will tell you either all good, the properties hold in the model, or they'll tell you nope, and they will give you a behavior, a sequence of states that lead to that property being violated. So this is like the core, very high level of things. And then what QUINT is is the model and properties. So the language is this. And, and the QUINT also provides uh, simulation and integration with model checking. But the language, uh, defines models and properties and then the models. It's very abstract, but uh, let's make it a bit more concrete. So models are state machines. Like when we learn about an initial state, which is a node, and then you make a bunch of transitions and then you have this state machine. Um, so the usual way of writing state machines in literature is like this. You define what are your states, for instance, 1 to 5 define what are transitions. So you can go from 1 to 2, you can go from 2 to 3, etc. And you define what are your initial states. This is how you define a, ah, state machine, or more precisely a transition system. Um, and visualize it. This is I think the most usual way. You just draw something on a whiteboard, like some arrows and circles. But this is very like a lot of work for real systems. You cannot really draw a state machine for. You cannot even render, like some people try to render state machines to understand their systems. And it's only useful uh, if the system is really small. If it's like a little bit more realistic, then you cannot even like see all of the states, it's too many. So definitely not drawing them by hand would not be feasible. So in QUINT is just a language to make this, um, more powerful. Define this in a more powerful manner. So this is how we would define this in Quint. So we start with uh, so you have a variable which is an integer. You start with that variable being one. And then your step here is defining all of your transitions. So it says X in the next state is equal to X on this state plus one. And this statement here defines all of these arrows, you see. So it's like you don't have to define each arrow on its own. You just have one way to define all of the arrows in a powerful language. So it's a language for defining, um, uh, your model Your state machine. And then you also write properties in the same language. So you can see like X is never equal to 42. That could be one property. Yeah. And then you can give that model, give the property to the model checker or the simulator and it will tell you if it holds or not. And if it doesn't hold, and this is very important, if it doesn't hold, it will tell you when it does not hold. Like this is exact sequence of transitions and states, this is when it doesn't hold. And therefore you can understand and, and you can debug. Uh, and there's no false positives. Right. Because if there is actually a violation here, then you can actually see what it is.

Speaker B: I see, yeah. Interesting. So this is interesting, uh, which companies are using. Well I mean Informal System obviously. And then Informal System came up with this. But like how is this being uh, applied how the company use it?

Speaker A: Yeah, uh, we have like a use cases list here. Um, a lot of these were written by Informal Systems for other people but some of them are external. So we have uh, several of these. One very interesting one, it's an internal from Informal Systems. It's a very interesting one. So Malachite is a consensus engine we developed uh, inside Informal Systems. The team there was really relying a lot on Quint from the beginning was almost like born out of Quint, uh, and they were specifying the whole protocol with Quint and making sure that, using model based testing to make sure that the code uh, followed what was defined in the protocol, sorry, in the specification. So they were, they were very reliant on Quint. And this was uh, last year sold or this was acquired by Circle. So Informal sold the software team uh, to Circle and they are now using that to build arc, their L. And it's being super successful. It's very stable, it's looking very, very promising. Um, and it was Uzo's project, uh, completely like I think the project in the world that mostly used Quint, uh up to this point was Malachite. So that's an interesting one.

Speaker B: I mean I see the Monad BFT from there as well. Like Byzantine, full tolerant Monad is a pretty big blockchain in the uh, Web3 ecosystem as well.

Speaker A: Yeah, we just finished some more work with for them. Yeah. And uh, it's a very nice use case and like it's such a complex protocol and how much we get to understand it uh, in Quint and get confidence uh, on the correctness. And then we found like some uh, stuff on their paper that Was not completely precise. And like the interaction between the team writing Quint and their designers is very interesting. Yeah. I can also show, um, something else. Uh, so what I explained so far is like how a lot of things are in Quint, everything centered on behaviors on these executions of the state machine. And this can be very high level. It's not the same as in your code. It's very hard to see what are the behaviors. Right. You can put some log lines there. Still, um, it's very hard to understand the behavior in a high level. And in Quint you're always staying on this high level and getting the behavior understanding. And this can be done even in the design phase before you have any code. So it's all very centered in behavior. But the way you get confidence behavior is how you get understanding, but the way you get confidence is by having evidences of confidence. And I have, oops, you saw my cat. Uh, uh, we're uh, thinking about three types of evidence that you can get out of Quint and we separate them into properties. Example runs in witnesses. Uh, and then some properties are the things that should always hold, should always be true. For instance, like, no two users can have both the same ticket. Right.

Speaker B: Or

Speaker A: having like a defi thing. You don't want any overdraft, you don't want anyone to have negative balances like these things that have to be true all the time. Uh, and you have like example runs. And is this something also we built like on top of tla, uh, that we value a lot. Uh, in Quint you can write like a sequence of either abstract or concrete steps that should be possible. So you can say like, it should be possible for Alice to book an appointment and then cancel and then book again and then reschedule. So you can say like, what is your happy path and how it should behave in your happy path and what are the expectations there? And then you can also say what are the corner cases you have in mind? So for instance, in like consensus algorithm, you can specify how disagreement can happen when you have too many Byzantine nodes or too many faulty nodes. Right? So how, like in a blockchain, how can, like if you have too many nodes being controlled by the same person, how does the attack happen? How do they take control? That's a scenario you have in mind. And it's important to document that scenario because that's what your protocol is concerned with. Right? You don't want that scenario to happen and that's why you have these different settings. But if there's too many, uh, Faulty nodes, too many nodes that are compromised, then that scenario can happen. Happen. Um, so that's very useful to document what those scenarios are. And then when other engineers are writing the code, they can consult also this documentation that there's. There's executable documentation. Um, and the third one is just witnesses, which are just things that should be possible because it's very easy to write a pro, a protocol that for say, for instance, like no two users can have bought the same ticket. It's very easy to write a protocol that does this. It's just no tickets are ever sold at all. My product is satisfied. Right. But then it's not doing anything interesting. So itnesses is the. It's the counter thing here. So we can have. There exists a scenario where actually people buy tickets or there exists a scenario where two people have added the same item to the same cart or to their cart. Um, so it's um, some way of defining specific scenarios without having to say how we get there. Uh, and then we can check that those actually happen. So when we are writing those three things or thinking about those three things, we are getting evidence of confidence. And I like the word evidence for this because it's different than proofs. We can have proofs as well, but not necessarily do we need proofs in order to have confidence. Sometimes evidence is enough and sometimes it's like getting to a proof would be a lot of work, but the evidence is easy and it's enough. Uh, I already have a lot of confidence, so I like the word evidence for this.

Speaker B: I see. Yeah. So these are pretty much very important, uh, things I mean, need to hold in Smart Contract and Web three. Yeah, I can see that this is actually widely applicable, but obviously. So would you say the queen is like, uh, this would replace MacDow like you said. And a lot of the InDesign docs would you say yes, and then insert there, which is right with quint.

Speaker A: Yeah, yeah, that's pretty much, uh. Oh, I also have like a slide I can use to. It's one of my last slides. Sorry if it's flicking the screen a lot. Yeah, here we are. Uh, so, uh, when you start with your design, you have like an intent of what you want to build.

Speaker B: Yeah.

Speaker A: And, uh, if you start transforming that intent into an executable specification, and here you can leverage AI a lot for this, you definitely don't have to be writing everything by hand. So you interacting with AI and saying like, oh, this is what I want to build, but make sure you have a quinspec don't just come back with a markdown document. I don't want that. Come back with a Queen spec. So I want a system that does this and et cetera. And then when the AI is writing the specification for you, it will like, oh, do you want this to hold? Like, do you want that? Or do you want this because it's forced to be precise on what it is defining. Well, markdown just allows AI to write anything on it. Quint will be forcing the AI to be precise and the AI will naturally come back to you with like, oh, do you want this or that scenario to happen? And then you are like, oh, actually I want this. And your design process is much more insightful. Uh, when you're having this formal specification underneath and then having all of these behaviors and you can see how the system behaves super early. When you're still like, in the realm of ideas, you're already seeing some behaviors happening. But when you're done with that and you have your specification, you're happy with it. Then it's a better artifact to generate code because it's more precise than just some English. It's, uh, artifact that can also generate test scenarios for you and test expectations. So you can make sure that the code is actually doing what, uh, it said it should do. And you can also use that for runtime monitoring. So you can see our application in, uh, production is also, uh, behaving as you had an intent in the beginning. So it becomes like a more of a holistic artifact because it has all of these powers. It's not just English. English cannot be this holistic artifact unless we become really good at reading and we can really spot everything just by reading English. But I don't think that will be the case.

Speaker B: I see. Yeah, that makes sense. Yeah. So, um, interesting. So, I mean, obviously you probably work with many different teams, right? And then, um, companies on this side. What do you say is like the biggest misconception that engineers I have about formal specification tools?

Speaker A: Interesting. Um, I think like people, um, they want more confidence. That's the pain that they're feeling. Right. They're not feeling confident enough. They want to feel more confidence in order to ship the skills software. And they think, okay, formal verification is going to help me. Uh, and they come start using Quint or other formal verification tools with this, like, hope of having verification. But they get so much value already just by writing the specification and just by thinking of things in more precise terms. A lot of people we worked with have been, have told us that they found, uh, problems in their design only by writing Quint before even running anything, just by being forced to be precise, they already found, uh, problems. So I think that's, uh, the biggest misconception. Like people think that verification is the only solution and proofs, foolproofs, and absolutely no bugs will ever be found. That's the only thing that will help them. But they get so much help along the way even before that. But I think that's super valuable and you should get to that at some point. But just like people, uh, don't expect how much value they can get even before that point.

Speaker B: That makes sense. So then if a startup is building distributed system, whether they're Web3 or Web2 or AI, whatever, and at what stage should they start thinking about writing specs, uh, in Quint?

Speaker A: Yeah, ideally as early as possible. Uh, I think, uh, Leslie Lamport, who created cla plus, likes to compare formal specifications with blueprints. When you're building like a building, like construction work, right. You never start building something without a blueprint. You first will plan what you're going to do. And the specifications, uh, for software are in a similar position because we often start building software before, uh, defining what we want to do. And then we have to rebuild things over and over again and we think, okay, that is cheaper than rebuilding an entire building. Right, it's cheaper. But is it really? Because when you are rebuilding stuff, you often introduce bugs and software engineers are quite expensive these days, so it's not, uh, that cheap. So that mentality of having a good design before you start building is important. So even, uh, for startups starting with distributed systems, I think it makes a lot of sense to try it out, see how it goes. With AI, it's pretty easy. Before, if you asked me this question one or two years ago, I will probably not be so secure, uh, saying this, so confident saying this because, okay, we're going to spend a lot of time writing the spec and learning the language. It going to be worth it. Maybe. But now like with AI, you can just try it and see if you can get value or not. Like in a couple of hours.

Speaker B: Yeah, yeah, makes sense. Yeah. Because with AI, I mean, like you can still use type in English or whatever your native language is and then get it to write for you. Yeah, makes sense. Cool. And um, so I guess how do you balance like the mathematical regal with the, uh, usability for engineers, right, who may not have a formal methods background or do they even need to have like a mathematics background?

Speaker A: Uh, mathematics background, uh, because you know,

Speaker B: like for an engineer, but most of the engineer. Okay, okay. Like, most of them may not have like advanced like math training, right?

Speaker A: Oh, yeah, no, definitely not. Uh, no. I think like, for instance, if you did like any uh, college in the area, you already have like enough math or probably like, if you pay enough attention to like high school, it's fine. Uh, so, yeah, so I think the most math things we use is like set theory. So like union and intersection and that kind of thing. I want to show uh, an example I have at the beginning here. I have too many slides, so sorry about this. Yeah, so in the bottom here, uh, I have how a CLA plus specification looks like. And this is what the syntax is mathematical because we say like in. So this value is in this set and then you have. This is very similar to math. Um, it's made for rendering in latex, which is what math people like. So this is a very mathematical syntax and this is the equivalent in Quint. Uh, and the idea in Quint is that first of all the operators are all readable so you can read for all. You don't have to know that a means for all. So you just read what's written there in English. Uh, and you can probably get, uh, if you have some experience in programming, you probably already. We can get what most of this is doing probably like action all in this, uh, symbol here are a bit weird, but everything else should be uh, straightforward. Um, we made this so people can read it much easier. There's no such thing as learning how to read Quint. If you already know programming, you should be able to read it fine. And there's also, uh, it should be easy to remember. This is less relevant now with AI. But our idea at the beginning is like you should. It should be easy to remember how you write things because it's not going to be the main language of someone, it's going to be their second language. They are like building something in Rust and then using Quint when they need to find some confidence. So yeah, I don't think any math is necessary. Like thinking about state machines and uh, maybe some set theory, that's all you need. Uh, and even here, this example, uh, is a bit on the other side, but we are still not seeing these symbols here and actions that much. You mostly see just normal functional programming and then you just go into this for a very small part of the spec.

Speaker B: Um, yeah, makes sense. Yeah, I think that'll be certainly very helpful not have to learn math because, um. Cool. And you said that teams have been actually been using Queen for quite some time. Right. To find bug. What is the one common class of bugs that traditional testing frameworks, maybe they miss, but formal specs using Queen can actually catch.

Speaker A: I think the strongest one is any edge cases. Because edge cases you either have to already know them, like in normal software testing you have to already know them and then uh, make a test for that. Uh, so you have to think about those yourself or someone will hit them in production and then you'll know the worst way. And there are tools like property based testing that help with that. But then property based testing is very attached to the code. While if you do what we do in Queens, it can be understood uh, with a simulator it uh, can be understood as property based testing for the specification. So it's a more high level and therefore you have more chances of finding those edge cases because you're only worrying about only on the scope of the things that are more safety critical, say a consensus protocol. So finding those edge cases, um, in consensus protocols, uh, in defi systems, um, those are what traditional testing often miss. Especially if you, we're not spending a lot of time thinking about what those edge cases are or if there's some very nasty edge case that you couldn't even came up with.

Speaker B: Yeah, that's true. I mean this is a very common problem in software testing. Right. I think humans you can come up with a lot of weird test case but there's always some even bizarre test case that would come up right in the middle when you run on production and then. Yeah, so anyway, that's quite good to hear. Just a couple of questions about the future I suppose. I'm curious about this. As you know, software system become more and more complex now that I give the output and productivity of everyone and just got to go up if they use AI. Right. So especially in the area like distributed system and blockchain. Do you think formal uh, specification will eventually become like a standard practice?

Speaker A: Yeah, I hope so. I think it's very hard to predict the future nowadays. I think it's like this few months is a, ah, very, lots of things are changing in the software world and it's very hard to predict. But how I'm thinking about this uh, currently is that I think some software will just be on this category of like we don't care about the code. For instance, like simple websites with not a lot of complexity on how the elements are positioned. Like we can just generate HTML with AI and probably be fine. You don't even need to inspect if Your HTML code is like, quote, unquote, um, correct in some way. It's probably fine. You can see the rendered page. It looks how you want it. It's probably fine. So I think some software will fall into those categories and then there will be more, like business people with no technical expertise writing some software. And in some cases that will be fine. M and there's like another category where, like, correctness is super important and if you don't do things properly, people will get hurt, money will be lost, a bunch of problems will happen. And there, I think there's less of a chance in some of that that we can ignore code completely or ignore how the systems behave and just trust that AI will do the right thing. And I think on that category, Quint will become very present in general. Other, uh, formal methods can be a good fit in some senses. But I think Quint addresses this confidence problem really well. Going back to what I said in the very start about what it does to your brain, what is programming even like? Programming is you're writing code, you're running it, and you're thinking about the scenarios in your head, like, am I covering everything? That is a very powerful skill, which is also very fun. And I don't think we are going to lose that forever. I think it's just changed a lot because we are not going to be typing all of the code and thinking about this while we type code anymore. I, uh, think it's a bit inevitable that this happens. Uh, but I believe that Quint can add this layer where we do the thinking and then we don't have to write the code, but we can do the thinking. Interacting with Quint, interacting with behaviors, uh, writing evidence about the things we believe in and then, uh, have all of that good stuff without having to write code.

Speaker B: Interesting. Yeah, I think we already seen the current days where a lot of the advanced developers. Actually I've talked to a lot of developers in some of the communities that I belong to and then it's like most of them tell me, oh, I don't write 95 or even 90% of my codes anymore. And just like, I just check. And then very little code is actually written by hand these days for the advanced developer. So I think that's really be the future. Yeah. Um, then I guess m talking about web3. There's a lot of smart m contract. Can you actually see that? Could formal specs actually eventually become a requirement before deploying critical smart contract? As you know, in Web three, smart contract get hacked, hacked a lot too much and so much like money is being at stake. Right. And yeah, uh, it's serious business right there and then. Yeah. Just curious, what do you think about that?

Speaker A: Yeah, I think Web3 so Quint was born inside a web tree company. Although it's not a Web3 tool, it's general purpose so it can be used in any scenario. But we found a lot of fit inside the web 3 community of developers because I think that just the nature of being decentralized already makes things so much more complex and these edge cases become so much more complex because when you're having edge cases in centralized software, it's one thing you can probably stop the fire, click a button. But when you have uh, edge cases in the decentralized systems, it becomes so much more complicated. There's so much more things you have to consider. So many different types of faults. So I think it's super interesting and it was a very welcoming environment for uh, us like for formal methods for Quint. And yeah, I don't know about having a requirement before shipping. I, I think like smart contracts where it's like the type of language and the type of environment where you can have very like uh, like formal, formal verification in the level of the language. So we have like formal verification tools specific to Solidity for instance and they're great and it's just justifies having like something specific to that language and even if it constrains the language, even if performance is worse or something, it, the correctness is the most important thing there. So yeah, I think this is not like a new idea. I guess lots of people have been like trying to like form a verification for Solidity, uh, and I think it's a good fit.

Speaker B: Yeah, I see. Yeah, makes sense. Well hopefully we'll begin to see fewer and fewer smart contract hacks, but I don't think that's possible. But anyway, just hope for it. Uh, cool. Yeah. Just two more questions before we close out the show. Um, do you have any advice, I guess for developers? This is mainly for developers who want to try out Quint. Any like quick start guy or like sorry, you want to direct them to.

Speaker A: Yeah, for trying Quint, I would recommend nowadays if you're into AI, if you're not into AI, go to the website, follow the tutorials, you'll be fine. If you're into AI and you want to get the fastest route, uh, we have this thing called Quint LLM kit. So it's a kit for you to like have agents and commands and et cetera that can help you get started and you just type. Uh, I think it's like slash start and then it guides you through the process. So I definitely recommend that route. But if you're, if you don't want to use AI, that's also fine. We have a bunch of instructions on the website and that will also be able to guide you through.

Speaker B: Yeah, I see. Yeah, I'm pretty sure that like probably 90% of the developers I talk to these days, they know some sort of AI. Right. It's like very hard to developer. But yes, I'm pretty sure most of them would probably go for the kid round. Cool. And final question, where can people follow you and all Quint? Feel free to share any handles and username where you want to follow.

Speaker A: Yes. Uh, so I'm Bugarella on Twitter. Uh, we have quintlang for the Quint, uh, account. Quint account is quite new. We created it a couple of weeks ago. So yeah, so definitely give it a follow and uh, Also stars on GitHub are much appreciated. Uh, so if you want to find Quint on GitHub and give it a store, we are also on Blue sky and uh, LinkedIn. I post a lot on LinkedIn so if you want to find me on LinkedIn, uh, also like slash Bugarella pretty much Bugarella everywhere. Yeah, I think those are the ones from mainly active on Twitter and LinkedIn and then Quint.

Speaker B: Awesome. Yeah, so we'll make sure to put all those uh, links down in the show notes, show description so that for the developers and people to follow. Once again, Gabriela, it's been a pleasure having you on the show today. I think you've taught me and also a lot of the audience about new things about formal verification system and at Queen. So uh, good luck with your new role going forward at Quint company. I think it's going to be pretty exciting, right? Yeah. Thank you for joining.

Speaker A: Yeah, thank you so much. Thanks so much for having me.

Speaker B: Awesome. And we're back to my studio. What do you think about Quint and the informal systems that Gabriela and her team are building? If you're a mathematics aficionado are currently using Quint to build complex system. Drop a comment down below. I'm sure that Gabriella would love to read. Uh, our team will be taking a short break with drums traveling and we'll come back in the near future. Uh, thank you for being a subscriber and see you next time.