#173 Susan Potter from distributed systems to functional verification

Transcript

⚠ The following transcript was automatically generated.
❤ Help us out, Submit a pull-request to correct potential mistakes

Susan Potter 0:00
If you're building applications, you may not have to think about that quite as much. But if you're building libraries and toolkits and things that other developers rely on, then that becomes even more important to think about these properties and to think about how correct your software is. So the stuff at the bottom and the middle layers of our software stack really needs to be more correct than the stuff at the edges on the leaves, and in many cases right most of the time.

Tim Bourguignon 0:33
Hello, and welcome to developer's journey podcast, bringing you the making up stories of successful software developers. To help you on your upcoming journey. I'm your host team building your own this episode 173 I receive Susan Potter. Susan is a software development team lead architect enabler hermetic and wear off many hats with a focus in functional programming and infrastructure engineering. Our current interests include practical use of formal methods for verification and risk management in software delivery, congruence, configuration management, and declarative infrastructure. Wow, Susan, welcome to the afternoon.

Susan Potter 1:15
Thank you. Thank you for having me.

Tim Bourguignon 1:16
But before we come to your story, I want to thank the terrific listeners who support the show every month, you are keeping the dev journey lights up, if you would like to join this fine crew, and help me spend more time on finding phenomenal guests, then editing audio tracks, please go to our website, Dev journey dot info, and click on the Support me on Patreon button. Even the smallest contributions are giant steps toward a sustainable dev journey. journey. Thank you. And now back to today's guest. I hope we gave into all those complicated words here. But first things first, as you know, the show exists to help the listeners understand what your story look like and imagine how to shape their own future. So as always, let's go back all the way to the old beginnings. Where would you place the start of your

Susan Potter 2:12
my dev journey. I think there were probably some things before this that led to this point. But I remember where I was in college I was doing, I was studying mathematics. And I love this band so much that I like want us to put up like a website for them. And I want us to put up their tour dates and like discography and that kind of thing. And I was doing static HTML at this time, this was back in the 90s. And it was okay, I wanted to build a database of this stuff and be able to render it in different ways. So I took a class on c plus, which I thought is what I needed to know for this sort of thing. And it was it wasn't the best language intro maybe. But for someone who only done a little bit of markup and nose, a little bit of what their way around the Unix prompt maybe. But it was like my first like real programming experience at that point, besides doing cube basic as a child on my dad's machine and installing Minix on his Windows box when I didn't mean to and things like that, besides those experiences, yeah, C++ in a noncredit sort of class at college, just to try and figure out how to put some kind of data online via CGI scripts and stuff like that. And I'm sure if I looked at it now the I would be able to poke holes in it security wise all over the place and be able to compromise the host and everything. And it would just be embarrassing and everything. But yeah, that's like how I started more seriously, like programming. Yeah,

Tim Bourguignon 3:49
what got you hooked toward taking this ball, this first step?

Susan Potter 3:52
I think for me, it was just about being able to do something useful, right to fill a need. So I, I don't know, for whatever reason, I thought, Oh, I really want to get this stuff online. I don't know why it made no sense at the time, other than I was spending a lot of time on this mailing list about them. And I thought, yeah, I want to contribute and do something. Yeah, I think for me, it was just solving a practical problem. And like I totally did it the wrong way if I was doing but at the time, this was a mid 90s. So I probably would have been able to get up and running building a database much quicker with Perl and not and I did actually eventually learn Perl after C plus and for some reason that was much better for me and so I went from C++ to Pell full by the way this is cool for right because at least the boxes that I was running I can't remember if pull five had come out at this point or not. But the boxes that I was running on they were FreeBSD type things they were they only had like pill full it's yeah as long as the pill full person for quite a while and then and then after. After I got the setup. It was as my the end of my second year maybe it was not the end My first year at college and so I, my friend said, Oh, are you doing an internship or something? Are you gonna go and work someplace over the summer? And it hadn't occurred to me at all, because I'm a maths person. And I just think, Oh, I'm going to study maths in my free time. And I thought, Oh, maybe I should get a job. Oh, maybe that's a good idea. So I went to the career fair. And then the person there says, oh, here are all of the internships that are listed. But most of them are gone already. Because basically, you're, you're lazy, and you came too late sort of thing. But then one of the openings was like this investment bank, and I had no idea what an investment bank was at the time. And they're looking for someone, an intern, an intern for the E Business Technology Group or something like that. And I said, Okay, fine, I'll just shoot them like an email with my CV as it was, or whatever it is. And in my CV was on my website, which also had this garbage, so the band stuff, and I find I make the interview, and I go down to London for the interview. And the it's all really posh. It's like in Canary Wharf, like these really high rise buildings and everything. And this is totally new to me. I'm a scruff bucket usually. And so I go in at the reception, and then they say, Oh, you're doing here, and I'm like, I'm here for an interview. And I don't really know what I'm doing. Anyway, I eventually finally get to like, but ninth floor or something like that, in this gorgeous corner office with that's overlooking everything and, and then I'm just waiting there for my interviewer. And my interviewer comes in, he's got this really nice suit on and everything and he comes to shake my hands, and I shake his hand. And he says, Hello. And so we do the pleasantries and everything. And I sit down. And my, his first question for me is, who was garbage? The band that I was doing all of this discography tour dates for? And I was like, Oh, this is so embarrassing. I have no, I don't know how to respond to that. Anyway, for some reason, they actually liked how much I learned on my own to build this sort of stuff up. And so they eventually hired me. And so I worked for this investment bank I'd never heard of at the time, called Morgan Stanley, and for like the internship, and that's how I got started. And that's how, like, soon after graduating, I worked for a French investment bank called Powerball. And then after that, I decided maybe London wasn't for me. So I moved to, to go to a startup in San Francisco, which was right in the right at the end of the.com, boom, sort of thing. So that's like the very beginning trajectory and how I got started. But it all started because of this band called garbage that I loved at the time. And I just wanted to, yeah, learn how to put databases online. And that was it. Right?

Tim Bourguignon 7:48
Awesome. Shout out to them. When do you did you realize you were drifting from math to to computer science or software engineering? Stay with us.

Tim Bourguignon 8:03
We'll be right back. Hello imposters, if you work in tech want to work in tech or are tech curious in any way you'll want to listen to this. We've launched a community of professionals who come together to share information and advice about jobs, roles, careers, and the journeys we all take throughout our lives as the designers, builders, fixers investigators, explainers and protectors of the world's technology. We call it the impostor syndrome network. And all are welcome. So find the impostor syndrome network podcast wherever you listen to find podcasts, and look for the isn community on your favorite social platform. Hashtag impostor network.

Susan Potter 8:47
Yeah, probably when I was skipping, like, working on the website, yeah. In, in my final year, yeah, it was, yeah, at the beginning of the degree. So it was a three, three years, typically in England. And so at the beginning, I was totally dedicated to mathematics. I had a few, like negative experiences with some of the lectures and the first year and then I was like, like feeling already turned off from pursuing this longer term, because I had actually planned on doing the Masters afterwards. And from the beginning, at least, and, and then by the second year, I was spending a lot more time in the computer labs and with my 20s 20 floppies, and putting, like, long multiply just a zip files on and taking them back to my computer because I didn't have a nice internet connection in my room. But anyway, yeah, so it was Yeah. So I think my second year I was realizing, yeah, maybe I don't want to do mathematics anymore. But at the same time, I hadn't fully understood that, like I could actually make money and do something interesting as a career with computers. I just saw it initially. Less something I could just do to walk to occupy my mind or to be busy or something like that to do something that I thought was useful at the time.

Tim Bourguignon 10:11
And at which point, did you realize all the did that flip and you realize that could be really something and carry you over the next 20 years?

Susan Potter 10:20
I think it was the internship at Morgan Stanley. It was like this plan thing. And for me, it wasn't total. It was. I don't know. Yeah, I was already late. It was total luck that I happened upon that internship opportunity. And I had no expectation that I would actually get it. I just thought others might be good practice. But yeah, the internship itself was pretty structured. And I met some really cool people, some other interns there that stayed in touch with them. And so I think at that point, that's when I realized you this can actually be like a a career and actually quite interesting, like a lot of different things going on, that can occupy my mind for quite a while and and maybe do something useful at the same time. Sometimes, although, I think nowadays I feel the opposite. And maybe just discouraged. But maybe that's just the world around me the pandemic and everything. So, we'll see.

Tim Bourguignon 11:14
Okay, so let's put ourselves in this fork. Now you decided, okay, that might be the right choice, the right direction? How did you decide into into which direction to take into computer science or software engineering? There's, there's a plethora of ways. How did you find out which ways there are and decide for one and go with it?

Susan Potter 11:31
Yeah, so the my, my final year project, that university was on trying to distribute computation of like partial differential equations. And so it was I had already like, gone down this distributed systems like oriented thing, initially. And so that's what I was hoping to do going forward. And that's actually why I chose Powerball initially. And then I got this opportunity to move to to the startup that was doing sort of a peer to peer buyer seller type of network. And so I thought, yeah, this is totally what I really am interested in, like the distributed systems aspect. And in terms of learning the stuff, I mean, I hadn't actually done like, what I would consider real, like academic planning of this material until probably about five years into my career doing actually grappling with these things by hand, like in terms of reading research papers, understanding what's feasible and what's not feasible in different models of distribution and things that but I was actually just working towards just filling in the basic gaps that I had in terms of as I was working, understanding the better methods of doing things from algorithms to like, what kinds of data structures I really want to utilize for in different situations and why and that type of thing. And then for me, it was, I was much more following initially, like the white papers by the vendors, which kind of takes you to a bad place, maybe because then you're just like becoming a vendor fan girl, as opposed to actually understanding why you're, you're doing certain things. But yeah, I think for me, initially, distributed systems was a draw, often, the just doing something useful for getting data out and distributed systems has followed me all the way through. And today, I do much more infrastructure engineering slash like deliveries delivery pipeline setup, and trying to tune the development workflow and that kind of thing for multiple teams. And from that's interesting, because I'm coming at it now the distribution of the distributed system aspect from a human and team perspective, like how do we deliver more like across these teams and minimize the interdependencies or at least ensure that the things that need to be consistent are consistent across all of these things? That's been like really, actually fun for me to take it back to the human aspect of software development. And I've really appreciated that I think there is a benefit, of course, to going to focusing on the technical aspects of learning to the reading the research are really trying to apply it as well. And then deciding exactly where you want to apply that and how you want to apply

Tim Bourguignon 14:21
did get you right, so for a while you were really focused on the technical aspects of distributed systems. And at some point, you realize, wait a minute, I can apply that to squishy beats and beats to the to the human side of distributed systems, and you're reusing the same skill set, but now in a different context, bringing a different light into it. Did I get that? Yes.

Susan Potter 14:41
Yeah, no, absolutely. Yes. Absolutely. And it was, it's actually quite, it's quite fun and challenging in a totally different way, obviously, because you have politics of different teams and it depends on your organization, of course, but they can be a lot of politics, people reporting to in different reporting structures who are motivated by different things. And so of course, like you have to dangle carrots and maybe have a whip as well. And so you have to figure out when you dangle the carrot and when use the lip. So

Tim Bourguignon 15:14
was it was there a point in time when you had this realization that you can reuse your skill set in different contexts, or did it come gradually over time?

Susan Potter 15:24
It can gradually, about 10 years ago, or 12 years ago, I started moving more towards the systems aspect, not not just back end development, but also the operational aspects. And during that sort of period of adjustment, we can say, I recognize that Oh, like this, there's all of this trash that just gets lobbed over the wall. And like, everyone, no one's like these, these operational folks are complaining, and they've got a right to complain, because there's actually all of the slop and they have to clean it up. And it says, depending on the organization, there was a lot of janitorial work. Sometimes the developers would help and sometimes they wouldn't. And it again, dependent very much on the organizational structure. And so once I had seen a few different organizational structures, and how they differ in terms of the support for making something operational and making something sing for the user, because ultimately, we want to build systems that do a good job that are nice to use for actual humans in some capacity. And seeing the difference between organizations that just have these formal isolated janitorial jobs to make things operational. And then the developers go off to New Greenfield pastures. And the operations folks are they're trying to juggle like 15, like things, batons or whatever. And, and they don't really have the context. They don't have all of the contexts because they weren't the ones that originally wrote it, they don't actually even understand. And they don't even have documentation sometimes about what was the point what it like, why did we develop this feature? Or why did we develop it this way, any of those kinds of things, they don't actually have a perspective into that they don't have the background. And I'm proving things such that A that they did, and also making it such that developers were much more working with operational staff to understand the systems after it goes into production. It's not just some isolated NOC team that responds to alerts. And it's all of this manual stuff where they have to manually restart processes, because the developers didn't get the feed, I may not get the feedback. At some point, this is disconnection sometimes they don't get the feedback that this crashes every night or this crashes, every whatever, whether there's a slow memory, leak, bloat, whatever, or that the it's not doing connection management correctly, whatever it is, right like that. Often, it's just that developers aren't being told, like, they're not giving them feedback. And they're also not given the motivation to spend time on that. And so at that point, I think there was a huge push on the within the industry to focus on DevOps, and we're all big one happy family. I'm not sure that's totally materialized in every organization. But I do think that there is a there is a more of a path towards that enlightenment that we'll continue to work towards. I think there's a long way to go, yes. But it's a work in progress. And it's like diffusion of innovation. I'm not sure exactly what the innovation is, but like understanding that we actually have to be more collaborative across the different kinds of roles that we have, and trying to diffuse that across the industry more and more into more kinds of organizations and things like that. So that even the laggards are the ones that don't adopt the newer processes, the new kinds of technologies, they're the ones that are eventually do adopt it, too. So then we've increased the baseline sort of thing across the industry, but it's going to take a lot of time. And there's a lot of talk. And there's a lot of buzzwords, and we've already moved on to a new buzzword. So maybe I'm optimistic, but I do think at some point, it'll seep through the industry and the baseline will be higher, and we'll be able to do better things. But it's it's a work in progress. And there's so many other areas that we need to improve on in terms of software industry, right, like ethics and tying it back to what we're doing and understanding we've got this huge crisis environment crisis upon us and that we need to think a little more smartly about how we're using software to not just to help us minimize our use of things, resources and everything. But also do we actually need all of these devices? I don't know like where we're using up a lot of natural resources just creating the devices in the first place. But anyway, yeah.

Tim Bourguignon 19:58
If we're to or to just I'd be crazy for a minute if we use the distributed system that we are thinking on to the world as Oh, who do we get some interesting insights from there?

Susan Potter 20:08
Yeah, oh wait, many different kinds of systems that are joined, like in very subtle ways that kind of create these cycles that can either be positive or negative. And then I think that for I think we might get more insight from a systems thinking perspective, which is, like related, highly related to distributed systems. And, yeah, I think that the ritual world has to figure out how to limit our usage, right. So to eliminate some of the negative cycles that we're creating in the world and limit some of the extraction that we've we're doing, it's just broader, we just need to revisit a lot of our assumptions across the world. I think there's there's so many levels as well, right? There's so many parameters here, everything from geopolitics, all the way through to there's definitely some insight there. I haven't actually thought it through yet.

Tim Bourguignon 21:06
It was there was a curveball, I must use the term systems thinking, insistent thinking and distributed systems, we have the word system in there. And you said they're related, but not entirely. How would you define both? And how do they relate to one another? Yeah,

Susan Potter 21:23
the distributed systems that I'm the research that I'm familiar with, primarily focus on software, distributed systems, systems thinking is something that was developed by I think, mostly more educators and social scientists to describe systems that were could be human and possibly other things. But I think primarily human based systems to describe, you know, the interactions and the how the system evolves over time with pulling various parameters. So absolutely, that they're studying sort of the same phenomenon at some basic level. But they're they're focusing on to kind of separate realms, if you will, or points of application, I would say, I think there's, of course, there's a lot that can be extracted from model system thinking and into distributed systems. And we've got these more formal models to describe, you know, more mathematically, how these agents, these computer agents could interact with each other. On the distributive system side, but it there's a lot more. There's a lot more of the assumption that they don't have motivations, right, necessarily, and they don't have like allegiances and things like that. So, of course, it can be modeled in different ways. But the the assumptions are slightly different. I'd say, yeah, they're quite similar in terms of the nature of what they're studying, but they come at it from totally different angles.

Tim Bourguignon 22:54
Okay, yeah, it makes sense. Makes sense. I'd like to steer away from the from the system thinking, Oh, maybe we'll come back to it. I don't know. What's helped me in the Bible, I read for me, there was this message for verification. I remember a verification algorithm or the idea of verification of algorithms from university way back west. And since then, strangely enough, haven't heard a word of that. And that's the first time I hear it in 15 years. I'm a bit surprised. Is it coming back? And could you maybe describe what it is? And then get into the question is coming back? And then what about it?

Susan Potter 23:26
Yeah, I like reading about software verification research, I look at things like proof languages and things like that. That's something that I'm personally interested in being able to apply. I've applied it in a couple of ways. But I have to say, I'm not using it like that level of things in my day to day job right now. One thing that I think there's a spectrum, right, so we can move towards higher forms of verification, so verification, meaning that we can prove various properties about some software or some system. And we can do this in multiple ways. One of the ways that I'm familiar with is using proof languages or things like Agda, or address or CoQ do Q and things like that, where there are languages that allow you to describe a certain properties that you expect to hold always. And it will be able to do the verification for you like through its proof system to make sure that your assumptions are that your the properties that you specify, do in fact, hold according to to the properties that you specify. Now, there, there are some caveats here, there's always a way out, right? There's always an escape hatch. So you have to be careful with yourself with the way that you specify. So you have to have a specification and you have to be able to for example, you might want to say that you don't want this this to deadlock this this piece of software to deadlock and so you would come up with a way to express but it doesn't deadlock or whatever, like maybe deadlocking is really simple, it should be really simple to, but maybe you want to specify that there's no race conditions. And you can come up with ways to express that the value of the things that are being concurrently written to an area will always come back with the expected result, given various scenarios and simulations and so on. And you want to have higher assurance software, if various certain domains more than others. So one of the things that I am exposed to all the time is that oftentimes you can get away with a lot really bad software. Actually, software that doesn't do that isn't correct, it doesn't do what you would expect it to do, at least in edge cases, as you scale that software, and as you put it into different domains and settings, that do require higher levels of correctness, because it's maybe medical equipment or something along those lines, you do actually want to have some higher assurance, right. So if you're writing, if you're building, I don't know, an app that does something ecommerce see or something along those lines. Yeah, you don't want it to be incorrect all the time, obviously, like you would never get any users because no one would have a successful experience. But if you had a small number of edge cases, you could have like customer reps, respond to that and correct it on internal systems or whatever and work with the user. And if it's if it's only so much of the user experience a small surface area of the user experience, maybe it's not a big deal, like returns or whatever. But as more people get to use that, and that feature, or that experience that edge case, for some reason, then it becomes more and more costly to the company. Now in something like medical systems, you probably don't want someone's pacemaker to skip too many beats, or whatever it is. So you want to have these higher assurance, high assurance, like components and fit them together and make sure that they work together really well. And so of course, the surface area of that is much smaller, right? What it does, is perhaps a lot less, it touches less systems, obviously, when you would want it to and so on, because you don't want cascading failures and things like that. But yeah, it's it. Yeah. Okay, so is it gone, I think it's gone is probably not present in a lot of software systems, especially business commercial ones, just because they're all workarounds for for correct dealing with incorrect software, that, in the eyes of the executives, it's much more cost effective to just hire some people to respond to customers, and take care of them with the with the white glove. And whereas in other areas, you really do want some notion of correctness, right, whatever that is, and according to some specification, because if you don't, then there can be some really bad consequences for all kinds of applications. And okay, so where I'm coming at this from is I want to be able to go towards software verification, wherever I can and get higher assurance techniques and methods. So in between the proof languages, and Ruby there is there's a wide spectrum of things that we can do, we can do unit tests, even in Ruby, we can do unit tests. And then okay, unit tests are example based typically, now, you can also layer in there things like property based testing. And so property based testing, kind of gives you like a little bit more confidence, right? Because you're not just looking at the examples, like specific examples, if I give this input, I expect this specific output, you're saying, If I have input that have any kind of input that have these characteristics, that is generated using these kind of generators or something like that, then I expect an output that has these kinds of characteristics. And you can cover more of the surface area of what the inputs and also validate more of the outputs by using properties. And so this gives you higher assurance. And of course, you have to be careful with this too, right? Because you may you need to think about the coverage of these properties compared to like other forms of testing, and then what of course, everything is about just in context, right, you have to understand the context, you have to appreciate what it is that you're really trying to achieve here. And then from this point onwards, you can have you can model your data model using various type oriented like better type systems or dependent types and so on. And then once you get to that level, then you can do more of the proof stuff, right? Because dependent type systems allow you to do more of the to specify to validate to prove that you your specification actually matches your implementation and there's a spectrum and there's actually a lot more flavor that I'm not talking about because I'm not exposed to all of the forms of selfless verification. But I do think that like modeling, there is a place for things like in a property basis, money based testing and better modeling. It doesn't even have to be dependent types, but something towards like dependent types, you can get a lot of value out of just those methods and understanding like how algebraic data types work, and how you can actually use various forms of reasoning about parameter TriCity and things like that, which is a way to say, hey, there's actually only one way you can define this very generic function. And it will have, it always has to have this kind of property that always holds for it. And maybe that's desirable, maybe that's not desirable, in which case, you're modeling the wrong thing. But with these kinds of methods and techniques and AI ways of thinking about software, we can eliminate large, large parts of the software correctness surface area immediately, like at a much earlier phase of development, and then we don't have to worry about them when we're integrating systems. And when we're adding more complexity on the domain modeling side, and we can just focus on limiting what can go wrong and much sooner. And then when we do that, then I think we end up with something that's lower cost of maintenance and low cost of ownership long term. And then also, I think, you know, can at least if, if we do it, well, it can actually make the users whoever they are, like whatever domain we're in much more appreciative of the software that we offer or not even notice it. Ideally, I think, not even notice from the software at all. Yeah, at least not be constantly complaining about software.

Tim Bourguignon 31:41
Is is a good is a good first step it isn't needed. It isn't. And I'm glad you're talking about types, and then sticking at first this low level, because my feeling is that when we talk about verification, we quite often go very fast into more the on quite try to compare it to BDD and systems thinking in terms of verification. And I think it's not a fair comparison, that I'm not sure we're going to ever come to verification at the BDD level, like defining at a high level what a system should do. And having automata whichever, however, they it can look like, prove that for us, I That's not fair. But going a few steps deeper, I think there's a comparison to be done. And indeed, we could start verifying a lot of things automatically, either by generation by seeing the types, we saw the discussion when going from from JavaScript to TypeScript, that was a heated discussion. And indeed, the types are bringing some verification and some help in this regard. But I've always found it very difficult to put the cursor at the right level between BDD and so also behavior driven development, very high level development testing of all of our systems. And where do you put the new for verification? So I need to choose to see what's the state of the art nowadays?

Susan Potter 33:00
Yeah, I focus more on the functional side of this area. And only because I don't have that much time in the day, and there's something that I'm familiar with. But there's a whole world of this out there, there's different model checking, there's also model checking, right, like environments like TLA plus, and things like that allow you to model like a state machine or whatever, and then validate that the way that you're modeling it is, in fact adheres to the properties that you expect it to. So it's, um, yeah, and there's a lot of space in this. Yeah. And this is just a couple of the things that I'm aware of. So I'm not I should say that I'm not a verification like expert at all. But I do enjoy like reading this stuff and trying to figure out ways of applying small parts of it where I can. So for example, I may not apply proof, like I may not be writing most of my systems with a proof language or anything, but I do actually build models in Idris or Haskell and Haskell, maybe it isn't there, right? It's not a verification language. But I do model things in these languages first, because it gives me the ability to reason at higher levels, and I am able to and like the implementation languages that I'm typically

Tim Bourguignon 34:17
running in the bio I write as there was a second part, which was the congruent configuration management and declarative infrastructure. But that's a mouthful to say, is it easier to to go into verification in such a smaller area of software development?

Susan Potter 34:32
Yeah, I think you do need to focus your energies on ways of applying it or or go down the theory path, right? Like I'm definitely not down the theory path. I'm much more like a practitioner that has really specific needs, for example, congruent configuration for me something where you define like a system and in terms of an expression, and then that expression can get compiled down to an image and that image that is produced no matter where it's produced, will always produce the same image no matter where you are out what time you do it or anything like that. And then the and this eliminates a whole bunch of problems that I've seen at scale, when I've been trying to provision 10,000 hosts with Puppet, for example, the time at which puppet apply is run right is is critical to whether or not it will succeed or whether or not it will succeed and have the exact state that you expect it to. And so if you have any kind of drift, even if it's they will apply successfully, initially, you may have drift of packages across like these 10,000 VMs. And that may not matter this time that you applied it, but the next time that you apply it, it may actually matter, it may cause some kind of service failure because of different kinds of configuration that was pulled in with a slightly different version of package. And so those kinds of things, they happen a lot more and more readily at scale, when you're dealing with not just a large number of nodes that you need to provision on to but you need to be you need to be applying new kinds of changes over and over again, like more quickly. So it depends on the scale, right. So there's a number of nodes, and then how frequently that you need to be applying these things to. And if you're increasing either of those, you'll actually start seeing that the puppet, which is more convergent configuration management. And I just use that because that's where I saw convergent configuration failing at scale at a previous job. And that, so that kind of just fails. But if you're provisioning onto five nodes, and you can do it all at the same time, with some kind of distributed or sorry, parallel shell to all of them at the same time, not a big deal. Use what what you're comfortable with at the scale of five. But when you're dealing with much larger than that, that's when you actually have to start to think about the economies of maintenance and things like that. So

Tim Bourguignon 36:53
that's a whole new system for me. Put a single finger in there. That's fascinating. We had some Vagrant, we had some some puppet. But that was I was always like you said, Five, not 10,000.

Susan Potter 37:06
Right. Yeah, I mean, you should be like modeling the tools that make sense for you, right? Like, for your environment for what you're targeting, and that kind of thing. Of course, over time, things change, and they may change or they may not. So there's always this, this, this piece of luck in there that's infused. And so that that will that is the thing that's gonna, you might be lucky, and things don't change. Or you might have tried to bite off team and try to model a much larger system than you really needed to. And then you can suffocate on that complexity. Because really, you only have money for one ops person or like someone who's more offseason, like others. And then of course, you'll you'll suffocate on the complexity. And yeah, so you have to right size, everything, but it's hard. It's just and you have you need a lot of luck.

Tim Bourguignon 37:53
It sounds like some trial and error is, is maybe there and realize, oops, gone too far. That one's not firing up this time. And at some point, find a sweet spot. Yes. If you had one piece of advice for listeners in getting a few steps, not all the way but a few steps deeper into proving that what they coded is indeed what would be the first step you would describe for them.

Susan Potter 38:19
It depends on the background. I'm, personally I'm familiar with the functional programming realm of verification, and there's different branches. So I don't want to say that there's only one way but there I would be to learn about it. I would there's a few different places that are really good. I think Hillel Wayne, his name, sorry, I remember his Twitter handle better, but he's done like a whole book on TLA plus, and how to do model checking. So model checking is one one way in which you can check your your logic check that the model that you're trying to program is in fact, what you expect it to be right according to some specification. It's like a back and forth like process, like where you're, it's forcing you to specify, like what the model looks like and then forcing you like to interact with it to see to help you understand what it can and can't, what we can and can't ascertain about this model. Then there's more expressive type systems that allow you in like dependent type systems, but even before you get to dependent type systems, you can do more just even simple algebraic data types really helps me just we're start with something really simple, which is you've got a product or a some form of expressive enumeration you can call it a sum which itself can be can have arguments, right and multiple parameters. And, and it can even be recursive. So this model of defining our data types allows us especially if we can do ads like generic types in there where we need to like that allows us to define data types at least that isn't coupled with behavior, right we can add the behavior on top we can add Now we want to interact with that later through functions. And with this we can, there is an algebra behind algebraic data types, right? We have you, if you think about it, we've got something like a user. And it has a, like a user, username, and bio, and they're limited strings, they each have each of these components have cardinality of, there's only so many of these strings capable of being generated. So then because it's a product type, you just times the constituents, the cardinality of those constituents together to get the cardinality of the bigger thing. And you can do this over and over again, with the different forums. And so at this point, I actually understand okay, this so much information that I can pack into here, is it actually equivalence, somehow equivalent to this, this other type here, which could be a function, there's different ways that you can think of data and you can express it as data as data or data as functions or data's code. And so you can go in these many different directions. And yeah, there's a few different, you know, avenues that you can go, I would start with something fairly simple. And then think about the properties and then maybe build this property based testing libraries in pretty much every language now for being able to leverage that. And just think in terms of, oh, I only need to have a non empty list passed as input here to assert this, this property always holds on the output of this, this function, things like that will allow you to thinking more in terms of these general outcomes, we'll help you define like more well defined pieces of software. And of course, it depends if you're building applications, you may not have to think about that quite as much. But if you're building libraries and toolkits and things that other developers rely on, then that becomes even more important to think about these properties. And to think about how correct your software is. So the stuff at the bottom and the middle layers of our software stack really needs to be more correct than the stuff at the edges when the leaves in many cases right most of the time.

Tim Bourguignon 42:06
Amen to all of this and fantastic final words. Indeed. When you build libraries, you have to be corrective and more. Very, very cool. Soon, thank you very much. Where would be the best place to continue this discussion or start a discussion with you on verification or anything else?

Susan Potter 42:25
Sure. On Twitter, I'm so Sue's at Susan Potter on Twitter. I'm most available on Twitter.

Tim Bourguignon 42:33
Then people go there. You want to plug in before we call you today?

Susan Potter 42:40
No, thank you for having this is wonderful. Thank you.

Tim Bourguignon 42:44
My pleasure. And this has been another episode of the history. And we see each other next week. Bye. Thanks a lot for tuning in. I hope you have enjoyed this week's episode. If you liked the show, please share rate and review. It helps more listeners discover those stories. You can find the links to all the platforms to show appears on on our website, Dev journey dot info slash subscribe. Creating the show every week takes a lot of time, energy, and of course money. Would you please help me continue bringing out those inspiring stories every week by pledging a small monthly donation, you'll find our patreon link at Dev journey dot info slash donate. And finally, don't hesitate to reach out and tell me how this week story is shaping your future. You can find me on Twitter at @timothep ti m o t h e p or per email info at Dev journey dot info. Talk to you soon.