Ep. #61, Such a Beautiful Craft with Gabriela Moreira

From Programming Contests to Formal Methods

Rachel Chalmers: Today, I'm thrilled to have Gabriela Moreira on the show. Gabriela is co-founder and CEO of Quint, a behavior analysis layer for AI-generated code. A formal methods specialist, Gabriela started out in type systems and compilers research and built tooling for TLA+ through her bachelor's and master's studies.

She taught formal methods to undergraduates, then spent four and a half years at Informal Systems, where she co-created Quint, an executable specification language that brings the rigor of TLA+ to working engineers. Quint has spun out of Informal as its own company in April 2026, Generationship's excited to be an investor, and there are already 5,000 public files in GitHub in the Quint language. Gabriela, thank you so much for coming on the show.

Gabriela Moreira: Thank you for having me. Very excited to be chatting with you here.

Rachel: So you're a nerd to the bone. You've said that you've got hooked on programming contests where code has to survive inputs that you never see. Tell us what that taught you.

Gabriela: Well, that's pretty interesting because it was really on the start of my programming career at the university. So I was not one of these people that started coding as a kid and then when they joined university, they already know everything. I was still learning how to code while simultaneously joining this programming contest, which was very, very exciting.

And then I learned to program in this environment where the tools were all the time telling me that I missed some cases. Because in these contests, they give you some examples of when you put this input in, you should get this output. So given a problem statement, you have to write a program to solve that problem.

And it has these examples, which you use to validate your program, and then you submit it to the platform, but then it will run way more scenarios than those few examples you had in the first place. And then you realize, oh, I forgot to cover the scenario where this number is bigger than the other one. Oh, I forgot to cover a scenario when the number is zero.

And it just tells you, nope, you missed one case, and then you have to go and figure out what case that is, and it's super hard. And you're like, no, I'm sure this is right in all scenarios. I tried everything, I'm sure. And then you're like, oh, that's the one I missed.

So imagine I was learning to code in the same environment where this was happening. And I was very excited about the programming contest. So I think that shaped my brain a lot in terms of very early on, knowing that I was not able to think about it all.

And that was always part of my learning day to day. Oh, it's hard to think about all the cases. And I was always wondering, which case am I missing? What did I not consider?

Rachel: And then in 2018, a colleague showed you TLA+ and you started building tools around it immediately. What did you see in TLA+ that most engineers miss?

Gabriela: Yeah, I don't really know how to answer that. I thought about it a lot. And my answer is, it was love of first sight.

It's an unexplainable feeling, something attracted me on just the language. And that is just nerding out. I think people can relate to nerding out about something.

I was nerd sniped, like, oh, this is so cool, and it just matches the way your brain thinks about problems. So when I was trying to figure out what I was going to do in my life, which college I would join or university, I couldn't decide between mathematics and computer science. So I really couldn't, and then I kind of arbitrarily chose computer science, but I didn't know. I liked both a lot, and then I ended up liking some parts of mathematics inside computer science, like discrete mathematics, computer theory.

And TLA+ was really the manifestation of that in my brain. So it was about programming, it was about software, but it was also a lot of mathematics. And it was all there.

Rachel: Logic and proofs.

Gabriela: Yeah, logic. My first semester, I had logic, mathematics and logic, where you learn about De Morgan's Law and that kind of thing. And I really, really liked it. I would tell my friends, oh, I went to this class. It was so fun.

And then at the end, four years later, when I was finishing my graduation, TLA+ came and it was great. So it was love at first sight, but I didn't immediately, oh, this is my whole life now. I was like, okay, let's get to know this person, this TLA+ tool.

And then that's when I think maybe I saw what other engineers missed there. Because then with this background of always missing edge cases and trying to find them, trying to worry about them all the time and the cases I didn't thought about.

And at this point, I was already working in the industry and I was working on web development, but the backend and distributed systems and queues and messagings arriving in different orders. And I would spend a lot of my time in calls with my colleagues, with my teammates. And we were like, okay, but what about this? Oh, in this case, it won't work. So we have to come up with a different solution.

This is actually most of my work, was just discussing these things. And it was so obvious how TLA+ would help there. Because we could, oh, maybe we just model our solution, what we think the solution is.

And then we let the model checker, the tools, find what we are missing. And then it tells us what we're missing. And then we consider that into our solution.

It's like where the activity I'm spending all my brain power on can be solved by this tool.

So that's what I saw.

But what I also saw was, there's no way I'm going to convince my teammates to use this super mathematical tool with this weird tooling where you have to first go and spend some time writing a spec, which is super complicated. And then we might get the value out of it. I will not be able to convince this, to spend work hours into doing this. It's too complicated, and I don't think it's a good fit for the industry.

Maybe let's make it a good fit. What are small things I could do to make it more feasible to explain to my boss why we should use this thing? So that's what I started doing, tooling around TLA+, try to make it better.

How Quint Became a Company

Rachel: So that's how Quint began, as an internal tool at Informal. Was there a moment when inspiration struck you and you knew that this was going to be a company?

Gabriela: Well, not me. I cannot take credit for that. It was my now leadership colleagues, my CTO, my COO, they were the ones that saw it. And it was like, now it's time.

And I resisted a bit at first. I'm like, I'm not sure. I like my company.

We tried making a product out of Quint for a long time. Also, we had Apalache, the model checker, which also developed internally, also tried to make a product out of that because we wanted to scale. We wanted to grow the team, work on this for a long time. But it was really tough.

Just making products out of languages in general, it's unheard of. Most people get funding from other companies. And we were kind of like, you're a language, right? So how do we make a product?

But then when AI started becoming a thing, I will be honest, I was very skeptical at first. We were like, oh, there's no way the LLMs will be able to do this kind of thing. No, it's too stupid. They're just autocompletion. But then they kept surprising me and surprising me.

And then Zarko, our CTO, was pushing for it. We should really look into this thing. And we looked into it pretty early on. And I think around when Claude Code came out, November last year, October last year, when it got popular, we were like, oh, all right. Now it seems like we can generate specs.

Because I was trying, every month I would go into the tools and try, can you generate the Quint spec for me? And it was garbage. And then suddenly it was able to, and they're like, okay, this is a game changer.

Because all this time with improving TLA+ versus starting Quint, on all of that trajectory, what we were trying to do is lower the cost of writing the spec, of getting to the point where you have the spec, and increasing the value. You also done a lot of things to increase the value you get. You not only get this, but you also get...

I started, in my bachelor's thesis, I tried code generation. So you also get a prototype out of the thing. And then I tried test generation. So you also get a bunch of tests out of the code. So improving value and reducing cost.

And suddenly AI came, and now the cost is almost zero. You can just get the spec for free. That's amazing.

So now it's time. That's the thing that, okay, now it's feasible. Because before it was really hard. It's super valuable, but before you get any value, you have to spend weeks writing the spec. So it was really hard to convince ourselves that that could be a product or a business.

But once AI came, okay, now we can finally get people to the state where they have a spec for their system and they can see the value they get. So that was the game changer for us.

Rachel: The industry has treated formal methods as a luxury or even a curiosity because of that big upfront investment of time in writing the specs. Now AI is generating code a lot faster than humans can review it. Can we still afford to treat formal methods as a luxury?

Gabriela: Well, I think it was a luxury because of the costs. So I think it doesn't even function as a luxury anymore.

When things get cheap, they are not luxury anymore.

And I think people sometimes might still interpret them as luxuries and then they just try to show them around, show off. They go and ask their AI to generate a spec and they're like, hey, I have a spec. And they're just showing their fancy bags out of luxury items.

Rachel: Look at my Birkin spec.

Gabriela: Yeah, my Birkin spec. I have a reputation with Hermes and I got this one.

So I think some people still try to see it as luxury, but they're like, hey, we know you just got that in half an hour with Claude. It doesn't work as a luxury. So you have to show me how it's integrated into your workflow and actually helping you. And I really like that conversation.

So it's not just this token, not just, oh, I have a formal spec, but, okay, how are you integrating that into your development? And, okay, generate the formal spec for your version of code now, but it will change tomorrow and next week. What are you going to do about it? You have to integrate it into your workflows.

And maybe that's the luxury now. Integrating the spec into your software factory, making that part of your workflow. And I don't think that should be a luxury for long, but that's what we are building for, to make that also something everyone can use.

Where the Hard Human Work Moves

Rachel: Perfect setup for my next question. If LLMs can draft a spec from plain English, where does the hard human work move? What should young engineers be thinking about to specialize in to guarantee themselves a career?

Gabriela: I wish everyone knew the answer to that or anyone knew the answer to that. But I think the hard part was never to write the spec per se. Just as well, people always say, oh, the hard part was not writing the code, the hard part was blah, blah, blah.

I don't think it also was writing the spec. It was knowing how to leverage the spec and getting the thinking about it really and understanding the system. So it's really the same kind of hard task that I was doing when I was doing competitive programming. It's like, okay, I missed this case. How do I change my solution to also cover that case?

But it's also, you're not only responding to that one specific case. You're doing something smart. If you find, oh, I'm not covering that case, you're not going to add, if that case, then do this.

You're going to rework your solution, redesign it to also cover those cases. And that's the fun part of the job. At least for me, and I think for a lot of people.

So this, making sure that bad things don't happen, trying to predict what will make the software maintainable, because it's a prediction type of work. Because we cannot really move the time machine forward five years and see if it's easier to maintain or not. But I have to project what we make the software maintainable now also with changes from AI, iterating and improving it.

Because one thing, again, is making one piece of software correct. And another thing is to iterate on that. Because if humans are using your software, you're going to iterate and you're going to have to improve. And that is also maintainability and thinking about this over time and continuously. So I think that's the hard part.

And it fits the LLM story as well. A lot of people make demos and it's super quick to make a demo and present something and then, okay, but now put that in production and maintain it over time. It's much harder. So I think that's the hard part and where the human work moves now. And I think specs can help with that.

Rachel: Yeah, I do want to dig into that a little bit. You said that that's the fun part, but do you worry as I do that junior engineers are not being encouraged to do that kind of systems thinking, to see the system in a holistic way and that we run the risk of losing that kind of architecture brain?

Gabriela: Yeah, I do worry a lot about that. I don't have much contact with junior developers. I didn't have contact with them this year. What I do have contact with is students from the university.

And I think a lot of good students, they go to this, on the university I studied, which is where I have most contact with. They do the competitive programming. And there they cannot use AI at all. They're just holding their keyboards and they have this, oh, I have to think about all scenarios, and they get super smart out of this.

I don't know what are the procedures or the day-to-day in the normal software development job as a junior that allows you to do that. And I know some people are doing, oh, you have to study with AI. So you ask AI to query you, to quiz you. And I know people are trying different things, but I really don't know what works.

I would really love a role in which Quint helps with that. And I think there are some opportunities if the person is willing to learn. So, oh, I'm not going to use AI for this part of the thing. I'm going to actually think about stuff.

I think using interactive tools is what helps. And Quint brings that interaction to this higher abstraction level. So I think there is room for Quint and other tools really to help there.

But it has to be thoughtful. We have to stop what you're doing. Let's go and help the junior developers learn. Or they might help themselves learn.

But it's also the career. What is your career even now? I'm not sure. So, so hard.

I wish I knew. People ask me a lot about, oh, my daughter is interested in joining your area. It's computer science.

And I'm like, okay, I don't know anything anymore. I could give you advice two years ago. Now I feel like I'm not in a position to give anyone advice in starting a career. Which is sad, but everything is changing.

Rachel: It's terrifying.

Empty Check Marks

You are on record as skeptical of magic check marks, these things the industry wants to have that, it passes this and therefore it's good code. Which of these check marks is the industry trusting too much right now?

Gabriela: So I think what they trust right now is what they always trusted a lot, including myself, which are tests. I trust my tests a lot. I am a formal methods person, but I do like my tests.

I'm not like, I will dump all the tests and go to formal methods. So I really, really like my tests. I will not let you take my tests away from me. They are very important.

So with something we already had, we are already used to trusting the tests. And then I realized recently that my trust in tests was gone in new projects, in greenfield projects. Because we are moving fast, prototyping stuff. And then AI goes and writes tests.

That's how AI learned how to do the thing. It learned from the internet, from GitHub. Everyone writes tests. It learned to write tests as well.

And then I'm like, okay, it's writing tests. The tests will look fine. Okay, let's move on, move on.

And then moving on with the prototype, we had 400 tests, 800 tests. And I was like, I don't feel confident in this. They're passing, but I have no idea what these tests are even testing. So if I don't know what they are enforcing, I cannot have confidence in them.

And when I go and look at those tests, they are terrible. Tests AI writes are so bad. And even the coverage metrics we have for assessing test quality or test coverage, they don't help here because the tests are covering all lines of code, which is the most basic metric we have. Even if you do mutation testing, they might catch mutations. But they are also so sensitive to change that if you change even a small thing on the code, you have to update the tests.

That's not ideal because then you are always updating the test and they're not really helping you prevent regressions and those kinds of things. Especially if you cannot understand the test. And it's much harder to understand what the test is asserting if you don't read the code. If you're not on the habit of reading the code for every PR, which most people are not doing anymore, are moving towards a trend of not doing it.

So now you have tests that you don't really understand what they're asserting. Every single change in the code changes a bunch of tests, which is not really a problem because AI can easily update the test for you.

But then you end up with these empty check marks because you don't really understand what you're being protected of.

And so I was working on this prototype. I was, what is the feeling? I wasn't even scared. I'm like, oh, these are really bad.

And are other people also having this same quality of tests? Because it's really bad.

And then I went to work on Quint open source, which is more like a brownfield project where we wrote the tests, by hand, very well thought out. And it feels so good to work there.

I'm like, that's my vacation. And my weekend is open source. Everything's so calm here. My tests are great.

I can make changes. I can explore, the tests are there.

When I write more tests, it's good because it's also based. The AI can take the old tests as base for a new one. So they are also good, new tests. But in a greenfield project, just starting a Rust project as I did, the tests were really bad.

So that's my concern. A lot of people always, in our careers, we always relied a lot on tests. It's a very basic part of what we do.

And suddenly, the quality of tests is degrading very rapidly, and I'm not sure people are noticing.

From Simulation to Proof

Rachel: Lean-based provers chase complete proof. Quint is getting value from partial exploration in minutes per PR. Why is that the right bet?

Gabriela: Well, maybe this goes back to luxury a little bit. Quint would always be less of a luxury than Lean. Lean is the real stuff. So I think if you're people that are starting to adopt formal methods, should start with something more lightweight, experiment, and then move on to Lean.

And I think Lean is amazing. And ideally, everyone who can should move on to Lean, which doesn't mean abandoning Quint. Because the thing is, if you're proving things on Lean, you have to understand what you're proving.

And you might have, okay, you have proofs. Again, the empty check marks. Okay, check. But what did you check? If you don't understand that, it doesn't really help you.

So again, you have to understand what's being tested, what's being proven in order to have confidence, in order to get something out of those check marks. And I think just the Lean stuff is quite hard to read. It's quite hard to understand what's being proven.

While in Quint, you have something that's easier to read and also very interactive. So you can play around, you can touch it, see what happens. So if you get confidence that the Quint specification is capturing what you want, your intention, your behaviors, if you're like, okay, this is my solution.

Quint is a representation of my solution. Is it correct? You can do the lightweight verification, like a Quint simulation, which is what we do the most with Quint. It's very lightweight, run a simulation, find bugs, fix them. It's not going to give you verification, but it's going to give you confidence.

Then you can move on to the Quint model checkers, which are just the same as the TLA+ model checkers. You can use them, have verification.

And if you want to be really serious, then you can move on to Lean. You take your Quint spec and you prove properties about that in Lean. And ideally, we want to be in a position where you can do that directly. Right now, you have to translate your Quint spec to something called Veil first, which is a framework in Lean.

So translate that to Veil and prove that in Lean. But we want to have tighter integration so we can just use Lean with the Quint specs. So the Quint specs is what you are proving with the properties and stuff, and then Lean is just what helps you actually prove that.

Rachel: Oh, that's really cool. So your emphasis is moving towards the executable specs and then you're using Lean as the gold standard for the verification piece.

Gabriela: Yeah.

Rachel: That's a fascinating model.

Gabriela: And the more the industry, AI, advances into writing proofs and whatnot, then the more we can leverage that.

But I feel like it's an important step to first understand what your spec is saying to then go and start proving anything. And a lot of people jump directly to the proving thing, and then they end up with empty check marks.

Rachel: Well, thinking deeply about things is hard, Gabriela. It makes your brain hurt.

Gabriela: Yeah, but it's also fun.

Rachel: Yes.

A Trust Layer for AI-Generated Code

Every platform shift has had its trust layer, compilers, type checkers, CI. Can we make behavioral verification the trust layer for AI-generated code?

Gabriela: Yes, and the reason I believe that is what is going to happen is that we desperately need an abstraction layer.

And I think right now the options we have are either read the code, which is a bit too low level now for the amount of code that is being produced. And the other option is read what AI explains you about the code, which is usually unstructured text, which I personally hate, especially AI written text. Okay, I write human written text.

Rachel: Back to your love of logic.

Gabriela: Yeah. So, and the unstructuredness, and I think there are things you can do, like ask AI to render you a beautiful diagram of the thing. There are a lot of things you can do, and they are a bit ad hoc. And I think people are using that in an ad hoc way. So they try it, they post a demo on Twitter, and it goes to trash.

But there is no structure way. Oh, every time I review a PR, or the equivalent of that in the agentic world, I am going to review this level of abstraction. Or with this structure.

It's always text. The agent reports, this is what I've done. Text, text, text, and I have to read it.

And we are not good at reading. I don't believe that we, especially as developers, as engineers, we are going to find edge cases by reading the text of the AI reporting on what it had done.

So, I mean, it's some structure and some level of abstraction. So we don't care about all of the details on the code, but we do care about anything that might affect correctness. We care about how the software behaves.

It might have behavior that we don't want, that we want to remove that behavior and we want to make sure that it was actually removed. It's not possible anymore because that was a bug or a bad thing. And if you're introducing, oh, I want this to be possible, I want this behavior to happen, then we can also go and see if that behavior is there.

And we don't need to know what sorting algorithm was used for this thing or what kind of thing was used there or if you're logging things correctly. We just need to know what we care about. So we need to define, okay, these are the things I care about. And then whenever the software changes, I can, okay, what I care about, what changed. So we need a new abstraction level so we can understand what's happening.

Because right now, I think there's a lot of pressure being put on developers because they are still responsible for the code. They're still the ones that get paged in the middle of the night. If something breaks, they're still the ones who might get fired because something went super wrong. They're still the ones responsible one way or another.

But then they cannot do the same things that they're used to do in order to get confidence. They used to have a process and then suddenly, oh, you cannot do your process anymore because that's too slow, just move faster. And then there's no process for them to do and it feels really bad.

So I think we need some process in a higher abstraction level. So we can still understand, since you have a mental model of what the system does and understand how the system behaves, even if you don't understand every single detail, we still understand how the system behaves and can make changes confidently while we still own the responsibility of the software.

Rachel: It sounds great. Let's adopt it yesterday.

Gabriela: Yes.

Reading, Live Streams, and Lucky Breaks

Rachel: The three questions I ask everyone, what are you reading? How are you staying current in AI?

Gabriela: I'm doing a lot of reading of new stuff. On the AI side, my favorite ones, I really like the newsletter of the Pragmatic Engineer. Gergely Orosz does an amazing job.

I was watching a talk from him. He was summarizing what changed in industry, what stayed the same. And he was referring all the newsletters that he wrote.

I'm like, oh, I read all of these. It's a great summary. I feel like I'm aligned and I know what's going on.

And then as someone who doesn't live in the US, I cannot really go to the big conferences. So I'm very grateful that some of them post videos on YouTube. And I watch a lot of the AI Engineer talks for the AI Engineer conference. They also do in Europe and stuff. I watched a lot of talks from there.

And it's great because it's the biggest leaders, the top leaders on the AI native, now agentic tech factories. I've watched so many talks about the factories. It's all on YouTube. So it's a great resource.

Rachel: I'm in San Francisco and I love the videos because I'm a keyboard goblin and I like to not leave my house.

Gabriela: Yeah, I can relate to that. I know it feels completely different to be at the events, but also we cannot realistically be in all the events. So it's amazing that people post their events online. I'm so grateful.

I actually want to mention, this is one of the greatest, how our careers are sometimes made of a lot of lucky things that happen.

Rachel: Yes, yes.

Gabriela: And one very lucky thing that got me to where I am was an online conference. Because it was usually an in-person conference. And because of COVID, they did the online one. That's how I met the TLA+ conference.

And then the next year, they did the hybrid one and invited me to give a talk, but I couldn't travel. So it was a remote video talk that I gave. And that's how I got my job. So I'm very grateful for the online ones.

Rachel: Yeah, the great unsung benefit of the pandemic was it really collapsed those barriers for people outside the U.S. to access the conversation happening here.

Gabriela: Yeah. And then I have one last resource that's actually quite different and something kind of more new that I'm trying. Because I think on social media, on YouTube, people talk about how things should be and you should be doing this in the idealistic world.

But for my job, I really want to understand what people are actually doing on their day-to-day. And something very useful for that are live streams.

So some people just live stream how they're coding with AI. So I'm not going to ask Claude to do this. Oh, no, I got this log. Let me ask Claude to analyze it in this way.

So when I find these live streams happening, I think it's very useful. And it's just having it on the second screen while I do something else. And then sometimes, oh, that's interesting. That's an interesting way of doing things. So I can see more realistically what developers are doing.

Rachel: I haven't heard anybody talking about that before, but that's obviously genius. A brilliant way of staying current with the state of the art.

Gabriela: I used to watch a lot of gaming live streams, so it was a natural pivot for me.

Rachel: Yeah, I worked at Alchemist for Ravi, who his first big investment success was Justin.tv, which turned into Twitch. So, yes.

Gabriela: Wow, yeah.

A Five-Year Vision: Loving the Work

Rachel: Speaking of aspirational visions of the future, if everything goes exactly how you think it should go for the next five years, what would the future look like?

Gabriela: Well, I think it's very related to the conversation we were having about junior developers and people trying to find a career. And lately I've just been thinking so much about my job and really how much I am lucky to love so much what I do. So I feel like the thing I aspire to the most is for most people to love what they do for a living or at least find a hobby that they like.

I feel like my generation, which is startup, I'm older Gen Z. So Gen Z onwards, we have a lot of struggles to find jobs that we like, and now we're not supposed to like your jobs or whatever. And then there's also no hobbies. It's so much harder to find a hobby.

And then people just go to a job they don't like and then they go home to their phones, which is quite toxic. I think that's quite sad. And one thing I would like to change is for people to like their jobs more than they do now or find some job that they like or a hobby. I guess you don't want to be obligated to like your job, but I love mine.

And then I guess the way this reflects into my work is with software. So how do we love...

Because I love the job of software engineering and I don't want it to die with AI.

I see a lot of people online saying that we are all going to become managers of agents. So if you didn't want to become a manager, now it's your time to become a manager of agents. And management is an amazing job, but a lot of people have chosen not to do that and instead become staff software engineers or pursue that career. And I don't want these people to have to become managers.

Rachel: Equal rights for keyboard goblins.

Gabriela: Yes, equal rights. Yes, please.

So that's just, when you ask what I went for the next five years, it's just what I've been thinking every day. I really want these people to not have to become managers or be slaves to the robots. And we don't know how the industry is going to move, AI, AGI, we don't know what's going to happen. But regardless of that, I really would like people to work on things that they like.

Rachel: Yeah, having agency, deriving meaning from the work that you do, it really is priceless. It's worth taking a significant salary cut for that, as I have in fact done.

Gabriela: Yeah, it's such a beautiful craft, software engineer. I'm so in love with it and we don't have to lose it.

Of course, we cannot maybe be in touch with the code as we were before, but what are the things that we liked about being in touch with the code and how can we lift that to this new reality where agents are writing the code? How can we still do the things that we enjoy and just use the tools as tools?

Rachel: A generation ship is an interstellar spacecraft that takes longer than a human life to get where it's going. It's also a biosphere, a complete ecosphere inside. I'm going to give you one. What are you going to call it?

Gabriela: Yeah. So this question, that's the hardest question you can ask to a entrepreneur. Naming things. Naming things is super hard. I already named Quint, so I think I'm done with naming for the rest of my life.

Rachel: Quint would be a spectacular name for your vessel.

Gabriela: I think it's a good name. I was watching the other episode of the podcast with Emily and Alex, and I loved Alex's name, Pathfinder. I just wanted to take, I wanted to enter her ship.

Rachel: Pathfinder two. We can have a little fleet.

Gabriela: But also I tried to have one original idea. I tried not to steal from them. Also the name from Emily, I believe. Loved Ted Lasso. But mine is Joy Ship, the Ship of Joy.

Rachel: Joy Ship. Oh, that's wonderful.

Gabriela: Where everyone can enjoy what they're doing for work and for their hobbies and enjoying life.

Rachel: People should love their jobs.

Gabriela: Yeah.

Rachel: Gabriela, it's been an absolute delight to have you on the show. Thank you so much.

Gabriela: Thank you so much for having me.