diff --git a/site/episodes/003-reed-mullanix.md b/site/episodes/003-reed-mullanix.md
index f0a532b..fa6f882 100644
--- a/site/episodes/003-reed-mullanix.md
+++ b/site/episodes/003-reed-mullanix.md
@@ -13,4 +13,856 @@ topics:
 - humility
 ---
 
+Reed Mullanix (00:00):
+It often feels like when you're writing Haskell, there's these ghosts that are
+haunting your program and where these structures are kind of showing up, but you
+can't quite put your finger on exactly what's going on. And category theory is
+the one who's doing the haunting.
+
+Sandy Maguire (00:12):
+Hello and welcome to the third episode of the Cofree coffee cast. I'm your host,
+Sandy Maguire. And today I'm joined by Reed. Mullinix Reed is a research program
+at the university in Minnesota. We works on proof assistance for cubicle type
+theory. I'm hoping to figure out what that means today. I met Reed when he
+answered my call to meet cool FP people as I traveled around the world. But
+we've been collaborating closely ever since. Thank you so much for joining me
+today, Reed, we've got a question for you. What the hell is a proof assistant?
+Like what does it do and why might I want to use one before
+
+Reed Mullanix (00:58):
+Getting into of this? I, I think it's important to really discuss what a proof
+actually is. Um, because I feel like a lot of people have sort of
+misunderstandings or at the very least no idea, um, what a proof actually
+consists of. Um, so the big idea here is that we essentially want to establish
+that some statement is, is true or provide some sort of evidence for its truth.
+Um, and the way we normally do that mathematically is we construct some sort of
+rigorous argument. And so where we start from some premises, I may follow a
+bunch of logically valid like deductive steps. And then we finally derive our
+conclusion and what a proof assistant is sort of does two things. The first
+component is we write our proof in some sort of formal language that, you know,
+for our intent and purposes looks like a programming language.
+
+Reed Mullanix (01:47):
+And then the proof assistant will walk through all of our steps and say, yes,
+this is a valid proof. Um, you didn't make any sort of bad logical jumps and,
+and everything sort of checks out. Um, and it also helps us construct the proof.
+So while we're in the middle of things, um, these proofs can get quite hairy.
+Um, and it helps to kind of have all the context loaded up in the computer. So
+you can sort of see all of the hypotheses we have, you know, what we're trying
+to prove, so we don't get lost, um, that sort of thing. Uh, and these are quite
+important tools, I think for two big. Um, the first is that, uh, mathematical
+proofs have gotten enormous these days. Uh, if you look at some, uh, papers that
+have come out recently, some of them will be hundreds and hundreds of pages long
+of just intense, gnarly proofs.
+
+Reed Mullanix (02:36):
+That really only a tiny group of people can really check the validity of, uh,
+and doing so involves a huge amount of time and effort and we're human. We make
+mistakes, um, and, and things slip through the cracks. Generally we're able to
+repair the proof somewhat, but it, it's still a bit sketchy to have all this
+sort of floating around, um, without, uh, being able to, you know, step through
+and, and verify it all. Uh, and the second, which is a bit closer to me
+personally, is for education. Um, going back to the previous point, a lot of
+people don't really know what constitutes or proof, so having a tool sort of
+there to handhold them and say, yes, what you're doing is correct the arguments
+you're making, make sense, great job. Um, and also to you through the process.
+So you don't get lost. That's, that's super valuable. Um, and I think can
+provide really great educational opportunities, both for, um, students of
+mathematics, um, and programmers as well. Obviously
+
+Sandy Maguire (03:33):
+Whenever I was doing math and university, it wasn't ever clear to me what
+constituted a good argument where I would just do some work and it looked
+convincing to me and then the TAs would disagree and I wouldn't get a good mark
+on
+
+Reed Mullanix (03:43):
+It. The way I think about it is if you had the world's slows compiler, where you
+submit your program or your proof, um, and then you wait a couple of weeks to
+get, uh, a feedback on it and say, yes, this compiled great. Or no, you made a
+mistake on line 10, go back and try again. So the iteration times can, can
+really suck. Um, and if you're trying to self-learn, there is no iteration time.
+You're kind of going out into the woods. Um, but there's no trails and, and you
+have no map. So it can feel a lot of the times, like it's just very confusing
+and you you're sort of lost and you have really no idea what you're doing. I, if
+it's correct or not,
+
+Sandy Maguire (04:21):
+Do you know of any cases in which this would've solved a, a problem, have there
+ever been like any proof that have gotten into the mathematical, can that turned
+out to be false later on and a bunch of work needed to be thrown away? Or is it
+more of a, a precaution rather than a solution to a problem?
+
+Reed Mullanix (04:36):
+So generally what happens is, uh, I don't know if you know this, but
+mathematicians, they're generally pretty smart people and they have pretty good
+intuitions as to why things are true. So most mistakes tend to be quite
+technical in nature, but the general sort of intuition is correct. So they can
+be repaired if we look back at the proof of, um, for most last theorem, uh,
+there was a, an issue in the argument that took, I think, two years to correct.
+It was incredibly technical and it required a pretty low, large group of experts
+to get into the middle of this a hundred page proof or so, and correct these
+extremely technical mistakes. So if, uh, Andrew wi had a, a great tool working
+along with him, we would've been able to catch that alone earlier and saved, you
+know, a couple of years of extremely technical work. So yes, it it's rarely the
+case that proofs are totally, you know, parable, but mistakes do happen. And
+they do require a high level of expertise to spot and high level of expertise
+
+Sandy Maguire (05:28):
+To I'm interested in your interest in proof assistance and have heard a rumor
+that you've been working on them sort ever, uh, even before you were doing it
+professionally, is it true that you wrote your own proof assistant in the
+university to help with your math homework? What did that look like and how to
+help?
+
+Reed Mullanix (05:42):
+So at the time I was sort of playing around with these tools and I, I totally
+fell in love with them. I I've said this many times to, um, people who know me,
+but they're truly the world's best, uh, puzzle video game. So I, I just was
+totally enamored with them and I thought, you know what, I'm a programmer. I
+can, I can write my own. And at the time I was taking a, a class in, um, sort of
+introduction to formal proof, and it's like, this is the perfect use case for
+these tools, but I need to turn in my homework as like latte tech files. Um, but
+most of them are, are quite simple, like inductive arguments or just
+manipulating sort of proposition logic. Um, so they're quite easy to automate.
+Uh, so I wrote sort of a, a tactic framework and had it synthesize latte tech
+proofs.
+
+Reed Mullanix (06:26):
+Um, so you could write out all your proof seizing, like tactic steps. So you'd
+be like, introduce this. And then I bet my tool consult is automatically, so I'm
+just type auto. And then instead of like core line language term, like you'd get
+in like rag or something, you got out latte tech, um, that you could then submit
+as your, your homework. And generally it required tidying up. Cuz the whole
+thing was, you know, essentially a monster hack. I don't know if you've ever
+tried to programmatically generate latte tech, but uh, my advice is don't um,
+but it was, it was fun and that was actually the, uh, the only 100% I ever got
+in my university career. Did anyone ever catch on, oh, I talked to the professor
+about sort of using these tools at the, the start of the, the term, um, and that
+she said, yeah, it's interesting.
+
+Reed Mullanix (07:14):
+Uh, I've seen these before, but you know, please, please don't submit first, uh,
+uh, as your homework. Um, but I, I think writing the tool taught me a lot more
+about proof than doing the proofs, whatever. So I, I think it would be
+interesting to have a class on, on formal proof for computer scientists where
+during the, the progress of the class, you develop a proof assistant it's, you
+know, quite small and restricted to a quite simple subset, but it really does
+teach you, you know, what these things actually are. Um, what valid
+manipulations are, cuz you do have to program, program them up to, to
+
+Sandy Maguire (07:49):
+Switch topics a little bit. You said offline that quote, I feel like I managed
+to make the computer an extension of my brain. I'm wondering what you meant by
+that
+
+Reed Mullanix (07:57):
+Most high school programmers have this sort of you moment of epiphany where
+they're able to run the type checker in their head and I'm not super into rust.
+Uh, I wish, wish I was, but uh, it seems like rust developers had a similar
+thing for the borrower checker. You can kind of just look at an expression and
+then, you know, your brain sort of lights up and says, yes, this is good or no,
+this is bad. Here's where the issue is. Um, once you sort of invested yourself
+in a proof assistant, you kind of gained the same ability, um, just with math
+papers and, and proofs instead. Uh, so if you're reading something, you kind of
+have this little thing in the back of your head, that's, that's parsing
+expressions thinking, how would I sort of construct this proof, you know, where
+the difficult's gonna be? And it's something kind of looks sketchy. It becomes
+quite obvious. Whereas, you know, earlier I felt I was in these situations a lot
+where I'd be reading something it's like, yeah, I guess that kind of makes
+sense. Yeah, this is confusing. And I don't know if it's confusing because it's
+confusing or if I just don't understand it. So I, I feel like this has really
+given me the ability to parse things a lot easier and, and uh, a better smell
+check sort of
+
+Sandy Maguire (09:08):
+Does that often work. I find that when I'll, I'll be reading papers or textbook
+or something and maybe something will be wrong in it. But my, in my internal
+experience is that, oh, I just am probably like not smart enough to understand
+this right now does having sort of fluency and type checking help solve that
+problem.
+
+Reed Mullanix (09:25):
+I think it does. Um, and as a last resort, you can always open up whatever your
+favorite tool is and type it in. And then the computer will say, yes, this is
+good or no, this is nonsense. Um, so there is sort of an escape hatch there, but
+I, I do think it is pretty reliable for the most part. Um, and the other thing
+it sort of gives you, which I think is slightly more valuable is, um, a sense of
+aesthetics. Like you see some proof that's super involved and gnarly and has all
+these crazy arguments. And you think about trying to program that into a proof
+assistant, you immediately are gonna throw off your hands and go, this sounds
+horrible. This is gonna take me like months or years to actually complete. Um,
+so you start trying to consider, okay, if I were to write this, how would I
+approach the problem? Um, so from that perspective, it sort of goes from like
+understanding to actually sort of interpreting this and playing around with it
+yourself. Um, in a similar vein, you can think of like algorithms, you know, you
+can have some terrible algorithms, this is a total hack versus the beautiful,
+elegant one that's, you know, lovely to reason about and all that. Um, so I, I,
+I think there's a parallel there
+
+Sandy Maguire (10:32):
+Do elegant proofs work better in some sense, I'm not sure if I, I really know
+what I mean by that, but it feels like when I'm writing an elegant program, it,
+it has fewer edge cases and it has usually fewer bugs because it's based on
+something more fundamental. Is that, is that true in proofs as well?
+
+Reed Mullanix (10:48):
+Yes. The main thing here quite similar to has is it's questions of
+compositionally. We wanna design things, such that all of our sort of
+developments composed together in, in these beautiful steps. So everything just
+sort of follows naturally and you don't need to get super involved every time
+you want to perform any sort of step of deduction or something. Um, and a lot of
+the time, this is all about sort of careful choice of definitions. Um, we can
+choose some sort of involved thing that's kinda horrible to reason about, or we
+can sort of change our perspective and say, okay, what's really going on here.
+Can I sort of take a step back and abstract over some of these details and
+consider something that's sort of fundamentally simpler, uh, throw away all the
+unnecessary stuff and, and really get at the meat of what's going on here. And
+by doing that, the problems generally kind of just fall apart. Uh, all the
+complexity can dissolve and, uh, you're, you're left with these extremely simple
+composable proofs, um, that are light years just loads of magnet or orders of
+magnitudes simpler to deal with. Um, and, and I find that quite rewarding. Um,
+and, and it really provides a good sense of understanding. And you've, you've
+realized, uh, I can sort of write this in a better way cause you've really
+gotten at the core of what's going
+
+Sandy Maguire (12:10):
+On, do the analogy there, picking the right types for an algorithm where if you
+have the right type, just everything falls out of
+
+Reed Mullanix (12:17):
+It. It is actually literally the same thing. These are dependently type systems
+essentially, and our definitions are for the most part types. So it is literally
+choosing the correct type and the correct representation for that type so that
+everything follows easily. So you are exactly correct there.
+
+Sandy Maguire (12:34):
+I, I wanna dig more into that in a moment, but first some idle curiosity and
+that's uh, have you ever tried doing proof assistance for like non mathy things
+like with relationships or jobs or nutrition or something like that? And if so,
+how did it work?
+
+Reed Mullanix (12:47):
+I feel like this is sort of the classic programmer nerd, snip, where it's like,
+I know how to use computers and know how to use all these tools. I'm gonna apply
+them to every single thing in my life. And for me, the two things I, I tried
+doing this for were, you know, like nutrition and running and both of these
+failed miserably. Um, you end up spending all this time sort of writing
+everything that you did down in whatever organizational system and sort of
+formalizing all these hierarchies and trying to make everything just elegant and
+beautiful. Um, and you spend so much time doing this and it's just so
+non-productive, but because you're doing work and sort of organizing thing, the
+part of your brain that sort of likes this stuff is like, yes, you're getting so
+much done, but really it's just wasted work and know you're not getting anything
+done truly. So it it's a boondoggle. In my opinion, earlier,
+
+Sandy Maguire (13:43):
+You were saying that math is the best video game. I'm wondering, how did you get
+good at math is the first step to getting good at something just like to make it
+fun. Oh
+
+Reed Mullanix (13:50):
+Yeah. The way I, I sort of operate is I'm totally content to spend huge amount
+of times like doing something as long as it's engaging in, in fun. Um, and
+specifically if there's sort of fast feedback, that's just awesome. So yeah, if
+you're able to sort of make things, not a total slog, um, are you able to sort
+of get into that quick feedback loop of, you know, I'm gonna try and solve
+something I've presented with an issue. Okay. I can, you know, take another step
+to solve that. Um, it's far more enjoyable and you learn far quicker than if you
+just sort of sit there, think really hard and go, oh, I guess that's kind of
+right. Okay. I guess I'm just gonna move on this little fishy. So I, I do think
+that a, the fun and, and B the fast feedback make a
+
+Sandy Maguire (14:35):
+Huge difference. Is there something about math that is sort of fundamentally
+interesting to you?
+
+Reed Mullanix (14:41):
+I, I wanna say yes. And I wanna say no at the same time, um, on one hand, these
+things do feel sort of very fundamental, um, and, and are like an excellent way
+of sort of thinking about either concrete problems or just sort of like general
+structures, uh, which is all, you know, quite lovely and all that, but at the
+same time, it's all totally made up. If you can't go outside and, you know, go
+hunting around in nature and be like, aha, a mono to Bush, pick all the OIDs
+that's my dinner for tonight, you know, problems all. Um, so it it's ultimately,
+um, a fiction, but it's a useful fiction and it's an entertaining fiction. So I
+I'm totally content with that.
+
+Sandy Maguire (15:22):
+Can you tell me what you're currently working on in your, your day job? What's
+the problem and how are you going about it? And like, what would progress look
+like?
+
+Reed Mullanix (15:29):
+So I work on cool team T, which is a, uh, research grade, uh, proof assistant
+for this thing called Cartesian cubicle type theory. We'll probably get into the
+specifics of what all those words mean later. Um, but right now I'm specifically
+thinking about, uh, three things which are, uh, records modules, and how do we
+structure like algebraic data types, which I might call induc to types for
+reasons, but you hear me say that thank ADTs. Um, and sort of the problem
+statement is this, uh, a lot of the times, um, in proof assistance, we have sort
+of these large bodies of work, um, and we need to organize all of this. And, and
+the fact that we've gotten to this point where organization is an issue issue,
+it's a fantastic problem to have, right? That means we're able to be productive
+in the tools. We're able to have, you know, large amount of people using the
+tools.
+
+Reed Mullanix (16:21):
+Uh, so fantastic issue to have. However, if you use any of these before, um, you
+probably run into the issue where the organizations kind of it fee to deal with.
+Um, especially when it comes to things like records where we don't have like
+record extensibility in most systems. So if I wanna say, like, here's what it
+means to be a Monod. And here's what it means to be like, uh, group or
+something. I need to duplicate a bunch of work or nest fields inside of things.
+It's just extremely unpleasant, um, and a huge amount of boiler plate. Uh, and
+the same goes for the defense between like, this is a OID and this is a proof
+that a specific thing is a mono. So you need to duplicate your entire algebraic
+hierarchy twice, sometimes three times to get this done, um, which is, is not
+great.
+
+Reed Mullanix (17:16):
+Um, on the other hand, uh, we have sort of algebraic data types, which also have
+this extensibility problem. Um, just sort of in the same way we would the Pasal
+if you want, like extensible some types for errors or whatever, but here it
+would be like extensible some types for syntax trees or extensible, some types
+for, you know, free do dads or whatever. Um, so we, we run into the same sort of
+extensibility issues here as well. Um, and also when you're in independently
+type setting and you want to think about sort of problems of modularity, um, it
+sort of makes sense to think about like a record or independently type record
+and a module are sort of one and, and the same. So if we solve the problem with
+records, we sort of solve the problem from modules as well. So all of these sort
+of issues seem to have this nexus point where if we're sort of crack that nut,
+everything else will sort of follow, uh, quite, quite naturally. And, and that's
+what I'm trying to crack right now.
+
+Sandy Maguire (18:18):
+Can I pause you for a second? It's not immediately clear to me what the
+connection between modules and records is. Would you mind just elaborating on
+that for moment?
+
+Reed Mullanix (18:25):
+If you think about like what a module is in a piece of software, it's just
+essentially just a collection of types and functions over those types. Right.
+Um, and if we have a dependently typed record, that's a thing with a bunch of
+fields, right. Where the fields further down can depend on the things earlier on
+the record. Right. So we can think about like, like taking a module, which is
+sort of the same sort of dependent ordered collection of a bunch of things,
+right. And writing that same thing as a big record, right? So we take all the
+types and we add those as sort of fields in our, our record and all the
+functions. We add those as fields in our record. Um, it's, it's sort of the
+same, I idea of let's scrap your type classes, just sort of taken up a whole
+level, um, to sort of encompass the, the module system as a whole.
+
+Reed Mullanix (19:20):
+Right. And this is sort of nice because if you think about them as records, all
+these features that we've normally have to sort of hard code or a module system
+can be programmable. Um, and we can manipulate modules as if they were just
+values, uh, which is a huge win. Um, both from an IM implemented perspective. I
+don't need to think about every single thing you would possibly want to do with
+a module and enumerate them in my module system. Um, and also for me, user
+perspective, if you wanna do some crazy stuff, uh, crazy meta programming with
+modules, it's, it's just valuable programming. There's no, you know, weird
+module language that you need to learn. That's kind of totally different. And
+has all these or arbitrary
+
+Sandy Maguire (20:02):
+Restrictions. Now you're saying your, your current job is to try and make these
+three features the same, like records and types and modules, is that
+
+Reed Mullanix (20:10):
+Correct? We're trying to solve the extensive bill and the, the lack of
+programability of all three of these things of records of modules and of, uh,
+inductive data types.
+
+Sandy Maguire (20:21):
+What does program ability of inductive data types
+
+Reed Mullanix (20:24):
+Mean? GC generics would be what I would consider sort of programability of data
+types, the ability to reflect on a data type and do generic program just on the
+structure of the thing, which is, I don't know if you've used GC generics, um,
+it's useful. It's extremely useful to be able to sort of work structurally over,
+um, data types and to sort of define things for free as opposing to having to
+write the boiler plate every single time. Um, and this is especially true for,
+uh, sort of independently type settings. If I want to prove something about sort
+of some sort of inductive thing, it'd be really nice if I could just talk about
+the class of all inductives of a specific shape, um, and use that to sort of
+automatically drive, uh, functions in thes.
+
+Sandy Maguire (21:13):
+One of the issues with GC generics is that it's aside the original types where I
+have this extra type family that constructs this thing, that reifies the types,
+but like that is a different thing than the type of self is that where you're
+getting with this?
+
+Reed Mullanix (21:27):
+Yes, that, that is it. So if you think about data types generally and records as
+well, I, I should imagine they're sort of separate from the, the rest of the
+system, right? Like I can't have, um, a function that sort of returns an
+anonymous data type, right. That's that's not something we can do. We can write
+something like that with like, uh, funk through fix points and all these
+Combinators, but I don't know if you've done that recently. It's not very like
+fun or readable. Um, so the idea is to sort of get the best of both worlds,
+where we get this sort of first class nature of, of inductive data types and,
+and not relegate them to this. I can only define them at the top level. And
+then, you know, I have to do all this shenanigans to do reflection and, and all
+that, um, while also retaining the usability of the original, uh, encoding and
+not having to deal with sort of funk their fixed points and all these sort of
+Combinators, um, by hand, uh, cuz that is basically unusable as been.
+
+Sandy Maguire (22:30):
+And so how do you go about making progress on this? Like, like how do, how do
+you organize your thinking and what is, what is like doing research here? Look
+like
+
+Reed Mullanix (22:39):
+My guiding principle here is how can we think about these things categorically?
+Um, what, what are the semantics? Because if you wanna design a system and you
+need to sort of think about what the meaning of everything actually is, if you
+don't have that, you're just sort of tacking all these ad hoc bits on and then
+just like praying to God that everything sort of works out nicely and that you
+didn't miss anything, but once you have sort of an understanding of sort of this
+semantics of everything, it's quite simple to sort of look at what you want to
+do and say, okay, well what does this mean from the semantics? Like how would I
+encode that there and then use those insights to sort of add things back into
+your, your system concretely. Um, so that sort of process of thinking about the
+semantics gaining insight there, and then sort of bringing that back into the
+more concrete world, um, that's sort of been my guiding methodology basically.
+
+Sandy Maguire (23:34):
+And so you're approaching this categorically. It's not entirely clear to me
+exactly what category theory is, and I'm not really looking for a tutorial
+necessarily, but, um, how does category theory help?
+
+Reed Mullanix (23:45):
+So the whole point of category for theory for me is it's how, how do we think
+about things in sort of an, an isomorphism infer way? Um, now that's two very
+scary words that are put right next to each other, um, and probably raises even
+more questions. But for me that means how do we think about things in a way that
+isn't sort of tied to their underlying representations? Um, cause once we start
+thinking about how things are implemented concretely, we can get sort of bogged
+down in the details and the specifics of this one encoding that we've chosen.
+Um, so by sort of moving to the domain of category theory where everything is
+sort of naturally, you know, we can't look at the internal representation
+because that's just not part of our language. Um, things are much easier to
+think about and it's much easier to realize, okay, what's really fundamental to
+the structure here and what's sort of accidental. Um, so for this specific
+problem, we want to sort of phrase things in this, this categorical language.
+And then we, we sort of realize exactly what is going of them.
+
+Sandy Maguire (24:49):
+Cool. That, that, that makes a lot of sense to me. Fine. My life is a lot easier
+when I'll use sort of semantic types that describe a number rather than the
+number itself, because maybe it's indexed in a different system or something
+like that. And so if I, if I can describe things based on their meaning rather
+than their implementation, my life is a lot easier in program. And it sounds
+like this is the same idea, but sort of mathematically
+
+Reed Mullanix (25:11):
+Yes, exactly. You don't wanna sort of get bogged down in the, uh, the
+mathematical bits that everything's built on top of cuz that's a, there's a lot
+of mathematical bits and B it's easy to sort of miss the forest for the trees.
+
+Sandy Maguire (25:26):
+Category theory is rather scary to me and I suspect pro to a lot of our
+listeners as well. It feels like the, the category theory of people have just
+gone off into the weeds of abstraction. And I'm sure there's a lot of value
+there, but it's, it seems to be quite hard to communicate back to us, to, you
+know, mere mortals in your eyes. What, what makes a good abstraction of a
+problem and how do you know that you're on the right track?
+
+Reed Mullanix (25:45):
+Yes. A lot of it can be quite abstract and I feel like lot of that has to do
+with, we are using tools. Um, a lot of the time that weren't developed for our
+purposes specifically, or sort of picking things off the shelf that were
+developed, you know, 50 years ago or so for some algebraic topology problem, and
+then trying to sort of wrap our heads around that sort of sands the original
+context, um, which can be difficult, uh, learning the abstraction without the
+motivation is, is gonna be hard, uh, regardless of the situation. Um, but for
+me, what sort of makes a good abstraction as opposed to, um, you know, a not so
+good one is that everything should sort of the proper that we want should be
+extremely obvious. Um, and the operations that we want should be extremely
+straightforward toy and the things that we necessarily don't care about, um,
+should either be not possible to even talk about, or probably extremely annoying
+to talk about, um, in the same way that like, if we're trying to describe or
+design some sort of API for something, you know, we generally want to like pick
+data structures and algorithms that are really good for the, the purpose that we
+need.
+
+Reed Mullanix (27:04):
+Um, as opposed to sort of just trying to cobble together, you know, the biggest
+API possible that could describe every single combination of things that someone
+might potentially want to do. Um, so it it's really about sort of filing down
+and, and sort of realizing these are the things I actually really care about.
+These are the things I actually need to be able to do, and these are the things
+I need to be able to reason about. Um, and then hunting based off those
+criteria, as opposed to just sort of trying to grab whatever due dad off the
+shelf, um, that looks like it might potentially fit the, uh, the problem.
+
+Sandy Maguire (27:40):
+And then whenever I try to go through category three books, I, I often get
+bogged down by, I just like how many widgets there are. I'm wondering if
+applying category theory in real life is sort of just learning enough widgets so
+that you can start composing bigger things out of them in interesting ways,
+maybe a different way of phrasing. This is like, what does category theory look
+like when you're actually using it an anger?
+
+Reed Mullanix (27:59):
+So I, I feel like the difficulty here is that it's, we're truly learning a new
+language and to be a able to you inform sentences in our new language, we sort
+of need to learn the nouns and the verbs and the adjectives. Um, so there's this
+definitely point of pain, um, where we feel like we're talking like some fourth
+grader who can, you know, kind of talk sort of, I guess fourth grader might be a
+little bit old. Uh, let's go with talk. Um, we can form sentences, but they feel
+really awkward and it's just like difficult. And we might say things kind of
+wrong or use not quite the right phrasing. And it's, it's, it just feels clumsy.
+Um, so we need to sort of get past that layer into like a point of somewhat
+fluency and then things become much easier. Um, so I, I don't have a great
+answer of how to overcome that initial sort of barrier of, of learning the
+language.
+
+Reed Mullanix (28:59):
+Um, I think a lot of it comes down to, uh, practice, um, a, a good sort of
+learning resource, um, that provides good intuitions. Um, but at the end of the
+day, um, like learning a language, it's, it's a lot easier if you're sort of
+immersed in it, as opposed to showing up to class, you know, every, like twice a
+week, and then never speaking the language outside of, you know, class, it's
+gonna be much more difficult as opposed to if you move to some, some country and
+then you're sort of forced to speak it and you're surrounded by it. It becomes
+much simply
+
+Sandy Maguire (29:38):
+Under this metaphor are, are sort of categorical, widgets, like cones and funs.
+And I don't, I don't know, I don't know, widgets like that, just that fill up
+the books. Are these more like sentences in the languages or are they sort of
+fundamental nouns?
+
+Reed Mullanix (29:54):
+Those, I would say are fundamental nouns, um, cones they're on the border, but
+especially things like func theres natural transformations, uh, limits co
+limits. Those are sort of the atomic parts of the language. If you don't have
+those, it's going to be very difficult to, to really say anything meaningful.
+Um, but sort of as you reach more maturity with, with sort of concepts, um, it's
+totally fair to see some chapter and just go, I don't care about this. This is
+not applicable to me. Um, I am never gonna need to use this, uh, in the same way
+that if, you know, say I'm learning French or something, do I really need to
+learn all of the French terms for like road repair? Probably not. I'm not gonna
+need to do road repair in France. Um, so I can just let that stuff slide. If it
+comes into my life, I will learn it. Um, but I don't need to go and, and work
+through every single chapter of a book. Um, it is totally fair to read things
+non-linearly, um, and only go back once you realize you need something,
+
+Sandy Maguire (31:05):
+What's the equivalent of knowing whether this particular widget is a, a term for
+road repair. Is there a way in which you can identify that for yourself or do
+you sort of need to go and ask the elders
+
+Reed Mullanix (31:16):
+The way way I can normally tell is I, I try and get an intuition for things when
+I'm reading stuff. My first thing that goes through my mind is, um, sort of what
+is this, what are they trying to say? What is this person trying to communicate
+to me? Cause they came up with this thing for a reason. People don't just like,
+sit back there and think really hard and just write random stuff down. Um,
+generally there's a reason someone invented something. So what is that and why
+are they presenting it to me? Um, and if I can't think of a good intuition for
+it, um, or I can't quite see the context in which it'd be useful generally for
+me, that's a sign that this isn't meant for me right now. Um, this was sort of
+meant for a different person in a different place, doing different things. And
+it's totally for that. I am sort of not the target audience, if that becomes me
+in the future, I know where to go. Now,
+
+Sandy Maguire (32:11):
+What would you say is the importance of mathematical analogies?
+
+Reed Mullanix (32:15):
+So at the end of the day, you're gonna need to fit all of this stuff in your
+head. And for me, analogies are sort of a compression algorithm for doing that,
+right? If I can think of this sort of cute little of analogy or intuition for
+something that is sort of expressed in a sentence, I can generally remember it a
+lot easier than some like, uh, this is really technical and involved. Um, and
+maybe I might forget the exact details of something, but if I can kind of get
+the vibes of what's going on, it's, it's a lot easier to sort of remember in the
+long term and, and actually be able to get use out of the idea as opposed to
+just, you know, having your eyes glaze over reading this thing eight times, and
+then you walk away and then 15 minutes later it's totally gone. So I, I think as
+you're reading, trying to do this sort of compression process, such that
+everything fits in her head is, is super
+
+Sandy Maguire (33:03):
+Important. Potential says that category theory is to has school as has goals to
+assembly language. And that's extremely inspiring if it's true. Do you agree
+with that characterization?
+
+Reed Mullanix (33:12):
+Uh, from that perspective? Yes. A hundred percent. I mean, there, it often feels
+like when you're writing has school, there's sort of these ghosts that are
+haunting your program, um, where these structures are kind of just showing up,
+but you can't quite put your finger on exactly what's going on. Um, and, and
+category theory is the one who's doing the haunting for the most part.
+
+Sandy Maguire (33:34):
+I'm not sure I have that experience of having ghosts in my code. Would you mind
+articulating that a little further? Like when might that occur or what, what,
+what's the telltale sign of a haunting
+
+Reed Mullanix (33:42):
+It's generally that like things start fitting together in a specific way. Um, so
+if we look at all the, the proof synthesis work I did with, with you on
+refinery, generally, there's sort of these patterns that are kind of hiding in,
+in the background where it's like, I can tell something is going on here, but I
+can't exactly pinpoint what, uh, and sometimes this may be like literal types.
+Like, Hey, I'm seeing this sort of composition behavior show up time and time
+and time again in this program, maybe there's something going on. Uh, other
+times it may be sort of more abstract, like, Hey, this thing is sort of
+preserving information in an interesting way.
+
+Sandy Maguire (34:20):
+Something that comes to mind on that front is, um, when I go to write like a
+function instance or a mono weight instance, or maybe a, Mono's a better example
+here because the compiler can't do it for me. It's extremely boiler play to
+write, but it's a thing that's surprisingly hard to automate is that sort of the
+sense in which things might be haunted?
+
+Reed Mullanix (34:38):
+That that's one sense. Um, but for me, the haunting normally comes sort of the
+definitions, but, and the functions, um, and the behavior of functions. So like
+a better example of a haunting would be like, homomorphism, um, they show up
+absolutely everywhere, but until you, you know, to go looking for them, you
+don't necessarily see them. Um, another example I don't wanna get too often in
+the weeds here, um, is sort of things that look like appreciates. Um, once you
+sort of know what appreciate looks like, um, you start seeing them absolutely
+everywhere. And for an example, that sort of high school programmers might be
+more familiar with once you sort of learn, you know, what a Moad is, you go back
+to a different language, suddenly the specters are everywhere. You know, you can
+see them all around. It's like, ah, I know what you are. I know what you're up
+to. Uh, I understand you now. Um, so a category theory just, it makes us into
+better Ghostbusters makes sense. Um, we're able to spot those ghosts more easily
+and, and realize exactly what's going on. Um, instead of getting tormented by P
+ghosts,
+
+Sandy Maguire (35:53):
+That's a fantastic way of phrasing it. And really to, to me drives home, I at
+least the feeling of what it is you're trying to articulate. I look at Python
+and you guys knew about monos or Mona. Like your life would be so much easier. I
+get the impression that maybe that's what you and Barto are trying to tell me
+about category theory.
+
+Reed Mullanix (36:10):
+Yes, the structures are there, whether you like it or not, you can try and fight
+against them, or you can sort of go looking for them and, and try and understand
+the structures themselves. And then kind of come back to the more concrete world
+with a, a better understanding exactly what you're doing
+
+Sandy Maguire (36:25):
+To get a little, a little more abstract. I'm wondering if your knowledge of
+proof assistance and category theory sort of influences the way that you see
+the, the world
+
+Reed Mullanix (36:33):
+On one hand. I, I think it's super valuable to be able to sort of look at ones
+sort of in, in different domains and just sort of zoom out to the 10,000 foot
+view and go, okay, what's sort of really going on here. Um, what are the, the
+sort of actual problems here and, and what's just, um, sort of incidental
+complexity that arises from these sort of root causes. Uh, um, but I, I think
+that on the other hand, it's sort of, that's a, a dangerous way of thinking
+sometimes. Um, because sometimes the incidental complexity is actually quite
+important. Uh, and I think programmers especially have this sort of bad habit of
+looking at other domains and going, ah, I am smart. Aren't I can solve this with
+computers. And it's like, no, no, the computers, aren't the issue here, buddy.
+
+Sandy Maguire (37:27):
+So what are the issues then?
+
+Reed Mullanix (37:30):
+Uh, I think it really depends on sort of the domain you're you're talking about.
+Um, and I see this quite often with sort of social and organizational problems,
+um, where someone will have some cool technology that they really love. Um, and
+then they try and go around and look for nails with their, their fancy new
+hammer. Um, this again mainly comes up with sort of organizational problems. Um,
+and cryptocurrency seems to be quite bad at doing this, um, where people will
+say, ah, this social ill, if only we had some sort of just decentralized way of
+organizing people with tokens and blah, blah, blah, blah, blah, we could solve
+all the world's problems. And it's like, that's not the underlying technology is
+not fundamentally the issue here. These are people problems, um, and, and sort
+of issues of personality and, and sort of personal conflict, competing interests
+like social or technology is, is just not gonna solve this.
+
+Reed Mullanix (38:29):
+These things have been around long before computers and people probably remain
+problems, you know, far into the future. So, um, but I think this sort of
+perspective is important is after you've sort of done the research engaged with
+the problem directly and sort of, you have a good understanding of exactly
+what's going on in the situation. You're not coming into it as some sort of
+naive outsider who can just solve any problem cuz they can write code. Um, and
+only then just the sort of zooming out and going, okay, what's really going on
+here. That's that's when it's valuable. Um, so I, I do think that it's important
+to be cautious about your own abilities.
+
+Sandy Maguire (39:14):
+That's good advice. I think for, for all of us, me, especially, I often
+frustrate my partner by, um, assuming I can just solve problems at her domain
+without really knowing anything about it. But you know, like you said, I'm, I'm
+a programmer I'm smart, so I can just fix things and it's a thing I'm working
+on,
+
+Reed Mullanix (39:30):
+But yeah, and I don't wanna say that programmers can't solve problems. Like some
+problems computers are really good at for instance, um, some of the stuff that's
+been coming out recently, the sort of, uh, using S and T solvers for various
+legal issues. Um, I think that's super fascinating and is a great application of
+like tools to help people, um, and sort of going off in a, a bit of a tangent
+here. Um, I think a lot of the issues that sort of the, the programmer brain has
+is that I'm gonna have, you know, people help the tools when it really should be
+sort of inverted. Um, you want to be making things for people in the domain who
+actually know what they're doing, make their lives easier, you know, sort of
+human focused, um, and expert focused design as opposed to just barging in and
+going, ah, you know, I, the thing my hammer look, it's so great and cool.
+Everyone should use it. Um, the best
+
+Sandy Maguire (40:29):
+Tool in the world doesn't matter if nobody uses it and if it's not a joy to use
+or if it doesn't feel like it solves the problem, then nobody's gonna use it
+even if it
+
+Reed Mullanix (40:37):
+Might exactly. And sort of looping back, we've had this problem with, with proof
+assistance for quite a while now where, uh, all the computer scientists were
+like, Hey, look at these nifty tools we made. Um, but we made them for us. Uh,
+and they're basically pretty hard to use unless you're an expert in dependent
+type theory. And, you know, you have like a huge deal and all this stuff. Um, so
+if you're a mathematician coming to these tools, it's like, what are these
+people doing? This doesn't look like the stuff I'm doing at all. Um, so I, I
+think there's been great work recently sort of reaching out to that community of
+experts and going, okay, what do you want, how can we sort of meet you halfway
+with the things that we've developed, um, and make them actually usable to you.
+Uh, and it's always quite interesting to hear what their problems are versus
+ours. Um, cuz often it's like, oh, I hadn't even considered that being an issue.
+Or we've been trying to solve this, you know, extremely har hair problem for
+like a decade. And it turns out you guys actually don't care about that. So, uh,
+oops.
+
+Sandy Maguire (41:45):
+What are some of the problems you see in the world right now? And you know, if
+you were the philosopher king, like what changes
+
+Reed Mullanix (41:50):
+Would you make? So again, I wanna lead off here with, uh, the fact that I, I
+don't really know anything. So take everything I say with a keeping he dose of
+salt, but the way I, I sort of see a lot of the problems right now is sort of
+the root cause is a lack of, um, sort of community in the ability to organize,
+um, to, to make that more concrete. Um, I think a lot of the changes we're gonna
+need to make on the coming years sort of regarding like climate change, um,
+inequity and justice are gonna be sustained efforts. It's not the sort of thing
+where you show up to a protest or something one day and then go home and then go
+look at all the good I idea we solve those problems, you know, 20, 22, no more
+problems. Yeah. Um, it's the sort of thing that requires sustained action that
+isn't just at the personal level.
+
+Reed Mullanix (42:47):
+Um, and I think that the way we have sort of society set up right now, it's
+quite difficult to be able to do that. Um, um, both on sort of the, the micro
+level of our, our cities are just not built for that sort of level of community.
+Um, and on the macro level where it it's just, it seems like all the sort of
+systems and everything are set up to sort of atomize people and, and
+disintegrate community. Um, so if I were, you know, someone had the terrible
+idea of giving me any sort of meaningful power, which you really should not, um,
+that would be the direction I would, I would push in is, is try and, um, regain
+a sense of committee and, and sort of rebuild the ability to organize. Um, and
+I, I don't have any concrete answers of how to do that. Um, like so and said on,
+on an earlier podcast, it's quite easy to point out the problems. Um, but giving
+solutions is, is harder,
+
+Sandy Maguire (43:46):
+But we, we also don't need giant macro scale changes. Like what are some maybe
+small things we could do in the way we live or in our communities that would
+maybe foster a better sense of community? Is it do just going and meeting our
+neighbors or, um, trying to find spaces to regularly hang out in or that sort of
+thing.
+
+Reed Mullanix (44:09):
+So I, I think a large part of it is trying to build space where you can just
+sort of exist without sort of having to pay some sort of entry fee or you
+anything like that. And not only spaces where you can just exist, having those
+spaces be sort of community organized and built for the community. Um, like
+right now, if you sort of think about it, the only place that you can really go
+and just kind of exist in the world outside of your house without paying for
+anything are parks or the library, both of which are awesome, awesome services.
+I don't want denigrate those. Um, I, I use both pretty regularly, but I, I think
+that we need more spaces like that. Um, more sort of cooperative businesses, for
+instance, um, with a, a real focus on providing services that the community
+needs and the community wants, um, and, and also having sort of local
+stakeholders, um, and real local investment in those sort of businesses. Um, so
+yeah, more, more ground up sort of democratic institutions, uh, at the micro
+level, I think is, is the way to start.
+
+Sandy Maguire (45:26):
+Is that a thing I can do without being like a business owner? Like if I host
+events at my house or something like, um, it seems challenging to require buy-in
+from lots of peers who, who might not get anything immediately out of it. And
+I'm wondering if there's a thing that we can do that might give the stakeholder
+is more immediate value. And I, to me that seems like how things are gonna take
+off.
+
+Reed Mullanix (45:51):
+Yeah. I think there's sort of two AEs. One can go here, it's providing more
+immediate, like, yes, this is something I, I desperately need or lowering the
+initial payout or sort of buy-in. Um, so on the, the, yes, I immediately am, am
+getting payout here. I think things like communities, disaster relief are gonna
+be super important. Um, especially in the coming years. Uh, if you've seen of
+like, I, I live in California right now and we've had some pretty gnarly, uh,
+history of wildfires. Um, and I, I think having community organizations that are
+able to provide sort of aid and disaster relief when that stuff does come up is,
+is super important, um, and can provide extremely immediate, like high value
+payoff, um, in, in sort of the short term. Um, and the other option is just
+making it very easy to get involved in these sort of things, um, making it so
+that, you know, if you want to sort of work at the local, like co-op or
+something just like couple hours a week or something that's totally fine, you
+know, um, make it so that it's not, I a huge lifestyle change to get involved in
+these sort of things
+
+Sandy Maguire (47:00):
+You say you might not be a good choice for ultimate power, but I think I'd put
+you in charge if it were up to me. So, um, I've got one last question for you
+today. Reid, what advice do you think would be most impactful if people in our
+circles were to sort of pick up overnight,
+
+Reed Mullanix (47:14):
+There are sort of two answers I would give you. Um, the first circling back is
+that it's easy to spend a lot of time doing nothing while feeling like you're
+doing something, um, and maybe try and recognize when you are just shaving the
+act. Um, and they're caught in these circles of, well, I'm putting all this
+stuff in this tool and all my energy into this, but ultimately I'm getting
+absolutely no sort of value or, or usefulness outta this thing. Um, so trying to
+self-assess these, these personal habits of yours I think is, uh, is good. And
+I, I catch myself doing this all of the time. I am not free of sin. Um, and the
+second I think would be to be realistic about your sort of self-evaluations. Um,
+and am I actually an expert in this thing? Um, does it make sense for me to sort
+of barge into various spaces and proclaim that I have the answer to all of your
+problems, um, and to realize that people who may do other things and think very
+hard about them generally, there's a reason that they do things. Um, sometimes
+there's not, but most of the time, if you sit and you listen to them, you
+realize that yes, that there are reasons that they do things this way. Um, so
+be, be more receptive to listening and be more, more understanding of when
+you're just running in circles.
+
+Sandy Maguire (48:46):
+How do you spot when you're running in circles? Is there a telltale song?
+
+Reed Mullanix (48:51):
+Yeah, generally when I, when I catch myself doing this, I, I try and explain to
+myself, okay, what am I doing right now? Why am I doing it? And if I can't
+explain that to myself in a coherent way, generally, that means what I'm doing
+is just a waste of time. Um, specifically the, why am I doing this? Um, it's you
+end up sort of working your way up the stack of like, well, I'm doing this
+because of this problem, because of this other thing I'm doing sort of all the
+way up. And then you realize the thing you were trying to do in the first place
+was just either a waste of time or incorrect. So making sure that you sort of
+check your call stack every once in a while is a good thing to do.
+
+Sandy Maguire (49:31):
+Thank you so much for being here with me today. I really appreciate you taking
+the time to, to have a chat.
+
+Reed Mullanix (49:36):
+Yeah, no worries. Pleasure.