#49 Self-Education in PL - Ryan Brewer
02:23:47 Share

Welcome to one more episode of the Type Theory for All podcast. As always, this is your host, Pedro Abreu, or as Spotify would say, Beto Abdu. Apparently, Spotify system to understand names is worse than Starbucks or something. So they call me Beto Abdu.

Thank you for our Discord community for pointing that out. I thought it was absolutely hilarious. If you guys want to be part of this amazing, amazing community of entrepreneurs on PL, type theory researchers, hobbyists, or, you know, just people who want to hang out and learn more about this kind of stuff that we do here, please go to our website, Type Theory For All. You'll find links to our Discord over there.

This year, this semester, we are always organizing some study groups on books and research papers. There are a couple of those going on, so make sure to join the Discord and check those things out.

In fact, today's guest is one of our members in Discord. We were hanging around and just having a good time chatting. And I was like, dude, you actually have some really cool stuff on being a self-learning PL person. So I invited Ryan. So Ryan Brewer is coming here.

for this interview we're doing today. He is actually a college dropout, which just makes things even more impressive for me. He has an incredible blog about PL, category theory, logic, and he's kind of like building a kind of new NLab. So like getting a bunch of incredible definitions from category theory and building this wiki.

It has some really cool stuff going on. He better defines his goals as making formal theory more accessible outside of ivory tower of academia and easier to put into practice where it matters. And obviously that deeply resonates with our goal here at Type Theory for all. So who better to come over and have a conversation, a chat with us?

He also has a couple of very, very interesting projects such as SEDU2, I mean, the first SEDU2 interpreter, SaberFVM, and Arctic. In this episode, we will talk about all of his projects, his trajectory becoming a self-taught NPL, compilers, and formal methods. He shares with us

the wealth of resource he used to navigate this sea of knowledge, which I think is really cool. We also have a brief but heated discussion on the ethics of science. So that was definitely something. And I think that's it. Before we get into this conversation, one last quick message before I... So I do not have to interrupt the show in any other moment.

If you enjoy this show, please consider donating to our Ko-Fi. Simply go to our website, typetheorforall.com and follow the prompts with as little as $5. You're already making a great, great contribution towards Ko-Fi.

our independence, our life as a podcast, and the growth of this show. I have great plans for this, and I really need and appreciate any and all support that I may get. So without further ado, let's get into this conversation.

Welcome, everyone, to one more episode of the Type Theory for All podcast. As always, this is your host, Pedro Abreu, and it's my great pleasure to be here hanging out today with Dan Ploukin. How are you, my man? I'm doing great. I realized that this thing that you're doing where you call out to me, it's similar to what Craig Ferguson does. You've seen this late show where he'll talk to a skeleton. I'm like the talking skeleton in this kind of bit.

Maybe that's a reference that is going over your head. But anyway, hi, I'm doing great. I'm pleased to be here. I'm pleased to have...

be back on. Well, here today, it's also my great, great pleasure to have Ryan Brewer with us. How are you, man? Hello. It's good to be here. Thanks for having me. So just to give a little bit of an introduction of what happened, we were hanging out at our Discord this week, and there is some really, really interesting, fun stuff going on on the Type Theory for All Discord. We are organizing some study groups, and there is this study for

PL semantics and some other stuff going on. I highly recommend for anyone who is watching this show to go there and check it. But so we were having this conversation about foundations, questions, semantics, and things started getting very interesting. And Ryan started talking about how he basically just learned type theory and programming languages by himself.

And I thought, well, let's get together and just talk about it. How is the experience for being self-learned and navigating all of these things of programming languages, which I expect that it's not easy at all, because it's still very niche. There is not many resources.

So I wanted, this is why we're here. And I wanted to start for you to give us a little bit of a background, right? And like, what's your story going into PL? And what makes you so interested to spend your time learning all of these things? Sure, yes. First of all, like self-taught, like learning it completely on my own is, you know, quite the way to say it. Because really, that means, you know, a lot of help from podcasts like this one that I'm really excited about YouTube videos online.

blog posts, communities, Reddit, Discord, and it's like, it's out there, you know, so I do want to like, encourage people to not feel too intimidated about this kind of path. It feels very, very intimidating, but usually that's just the terminology, right? Like, category theory terminology is completely...

impenetrable, but the concepts are actually very simple and elegant. I learned a lot from this podcast, so it's very surreal to actually be here and be able to give back a little bit. And I just wanted to say that. Thank you for having me. All right. So getting into PL, I don't have like, so I was in middle school and then I just really wanted to make a programming language. I don't even know how to explain how this happened. I mean,

I started with Scratch, right? I think a lot of people did. Or I started with Snap, which is like a Berkeley version. Scratch is MIT. And I liked making games and things. And I realized that these blocks that you click and drag to make a game, you can't actually transfer that very well to JavaScript or like a real programming language when you want to make a game there that you can actually distribute to your friends and whatnot.

And so I thought like, man, I know how to code. I know while loops or whatever. I was like, why can't I actually like build something? And my dad, again, is a he's a researcher. He got me into this stuff.

And he's like, well, you know, you could make a language that's like Scratch or something, but like in text and then compiles, whatever. And I was like, I have no idea what he's talking about, but like, that's so cool. People build these things. You know, even in college, I had conversations with people like at this point when I was pretty into PL and they were like, you can make a programming language. Like, I think a lot of people have this strange impression that the languages like Python and C and whatever are like,

god-given you know like they were there at the start of the universe you know

It's like hard to like, it's a valid question, right? Because of bootstrapping, whatever, right? Programming languages are made in programming languages, then then how was there ever a programming language? So, so yeah, it's this kind of mind blowing thing when you start to get into it. So what was like your first programming language? And when did you make it? In eighth grade, I had a project to do some computer science stuff, because I wanted to do that. And we kind of got to choose. And I

really wanted to make this a PL project somehow, but I didn't know how. And I didn't know anything about PL either. So Arduino, you can kind of send messages to it through a serial port from your computer. And so I had it just like kind of switch on the bytes that I sent it to do different things, you know, very like

I didn't know at the time, but very like bytecode style. Yeah, a little small talky also because you're communicating by messages. No, but that's like interpreted. It's interpreted code. But I mean, that's what small talk is. It's just this is the only way to give text. It's more like a REPL. This is how you give text to an Arduino without like connecting it to the internet and all that. So yeah, that was, you know.

Not really useful for anything, but felt cool, you know, motivating. So it was like a basically a bytecode interpreter that you'd made. And what could it do? Could it would like flash up lights or something? Did it have like loops? Did you have gotos? No gotos. I don't think I've ever really used goto for anything. So it would have just been like normal looking C code. Oh, you're talking about what the language supported? No, there's definitely no control flow. Absolutely not.

I didn't, I was not thinking about any of that stuff at the time. I was like 13 or something. I think there were, there were other projects through the years, but similarly silly, you know? And I think, okay, when people get into PL, this is what I've seen in the community. Everyone has this dream programming language they want to make, you know, that can kind of do everything and doesn't actually like,

need to deal with problems because it's like imaginary, you know? And like, I, I fully support people to do that. I think that's actually really important. And what's happened for me is I keep trying to make something like that and then like failing halfway through for whatever reason, or just deciding I want it to be totally different. And like,

you end up with what you want for learning anyway, which is a long series of small projects that are pretty different from each other. But they have this kind of north star of what you care about in programming language design and what's also just fun to work on. I've done a lot more type system work than back-end work. That's just a fact. And when I have to do back-end work, I kind of get bored and move on to the next project.

And I'm not the only one. Yeah, pretty much. I've been getting into abstract machines recently, but for the most part, we all have things that we would rather work on. All of these projects helped me with learning about type systems and whatnot. One of my early ones was obsessed with Go when I thought Go was just the greatest thing. I don't think I had really come into functional programming yet.

But Go interfaces are really cool and exciting. I was just trying to figure out how to do that. So are they like Java interfaces? Oh, so Go interface is like an anonymous Java interface. You just write them in line in the function type signatures and whatnot. And for example, you kind of have like an any type. I mean, Go has an actual any type, but you can just use an empty interface as something that accepts anything and doesn't have any methods on it.

Right. So it's like you get the normal subtyping lattice and all that, and it's kind of fun. It's very, very structural, structural typing. So going back real quick to your path into programming languages. So you learned how to program and you're already hacking around with this stuff much before going to college. But I assume you still went to computer science college, like some computer science course.

Can you tell me about your undergraduate studies? How did that go? Because it blows my mind. I went there completely raw. I didn't know much what to expect. I didn't know how to program and anything. How's the experience of already going into there with something in mind, right?

The main thing is that the classes, well, I didn't go to like a really like good college. So maybe it's different for some people, but like. Which one did you go to? I went to San Diego State, which is not UCSD. And it's a really fun school. I actually recommend it for everyone, but not because of the academics.

And I kind of knew the concepts they were talking about. Like, they were teaching Java, and I kind of knew Java. But like the concepts in Java are very familiar if you've just done a lot of C like languages, you know, and object oriented stuff. I started working at a startup in like, sophomore year of high school. So I've been doing quite a lot of coding over the years.

over the years, I guess. And I kept working with them even into college because it was remote. And it was boring, you know, I mean, like, okay, it was boring. But I did get the chance to be they call it an ISA there. But it's basically like a undergrad TA like helping with you get office hours, people come and ask questions and stuff.

And that was really fulfilling actually, was just like helping these people who actually, you know, solicited my explanations about computer science. Which course did you take? Oh, this was just like intro to Java or something like that. Those are the best because you can see how awesome students are and like, and they'll say something that like you're already extremely used to it. And it's kind of, for us, it's kind of trivial. And as soon as we'll be like,

oh okay and it's it's really fulfilling it's really nice one of the highlights of my life was explaining how uh you get a random number within a certain interval which is like you know the random number uh you know it's going to be zero to one so you multiply it by the length of the interview interval and then you add it by the smallest number in the interview interval you know

And people could not figure out why that was what you do to, you know, like why a multiplication and addition is how you get it to be within an interval. And I go up to the whiteboard, I'm drawing it out. You know, you see the light come on in people's eyes. I don't know. There's just something so magical about this experience that I don't know. It's,

not something I had really thought about in years. Yeah, man. For sure. I can feel it. I definitely know what you're talking about because the way that I describe that sense is because you're kind of giving the students something that nothing, nobody can take away, which is knowledge. Like you're just

like you just give this spark of insight in their lives that it's theirs kind of forever, right? And you can see when that moment happens, the pupils just go, it's beautiful. It's awesome. And maybe this is just me, but I'm sure when I learned that whenever I did years ago, I got really excited about it because it's cool how that just kind of works out so like cleanly, but tried to explain it to everyone around me and just was faced by like,

you know that's so uninteresting why do you care about that right like i don't know if that happened for that but that has happened for a lot of things for me so the the setting where people are coming like wanting to learn these things feels just magical you know where it's actually consensual in some way and i'm not just being really annoying

For sure, man. For sure. I love that. I love that. So then you also mentioned that you went briefly towards grad school after that? Yes. I was hoping to become a professor.

Because I had in my head this idea of maybe like Newton sitting under the tree with the notebook and an Apple falls or whatever, just sitting around thinking about these problems. I used to say like, I would love to be paid like a salary to just read and write papers. Like that is the dream come true, you know, because I, I read papers on my phone. I don't know anyone else who does this, but I, I just like zoom around on my phone and

with the PDFs and whatever, zoom in a lot. It's really nice with the double column papers. And as a result, I kind of do it all the time, just between activities throughout the day, between classes. And it's very much just a way that I fill my free time and get excited by these things.

I don't think now that grad school and professorship is quite as romantic as I imagined it. Yeah, that's what I wanted to mention, but I wanted to see where you were going. Oh, I was just... Here's the thing, all right? The realization is that I actually read all these papers now. I don't actually need to go to grad school to do that.

you know i i'm learning the papers that come out at popple every year and all that so it's like i feel like i'm keeping myself kind of up to date and there's still a lot for me to learn don't get me wrong but i'm learning it too and and i think trying less hard in school so the to cut to the punchline i did drop out uh eventually

But wait, where did you go actually? How was it? Who was your advisor? What were you working on? So I have never been in grad school. So no advisor. So you dropped out of your bachelor's? Yes. I did not have a bachelor's. That's even more impressive actually. So I mean, it was a very long drawn out process. So I did two years of bachelor's and then I took a gap year.

And then I kind of transferred to online classes and then I dropped out of those because I was just losing my patience with the whole thing over time. But dropping out is really hard, like just psychologically because of the taboo and all of that, you know.

So it took me a long time to realize that, you know, I'm already working. I'm not doing this to get a job like most of my classmates are. You know, I'm wildly romanticizing the thing that I'm putting so much effort into doing. And I might finish and try to do grad school later in life. But I just right now I realize that.

uh free time and relaxation are the things that i should be optimizing more because i'm exhausted or i was a few months ago but i i guarantee that we have listeners who are going through the exact same thing so you would give them a little bit of like schadenfreude if you would like to talk more about like what did you find so excruciating and like you get to relish in the fact that like now it's over and life is better like talk about what

If you don't mind, I mean, it is quite a personal question. One thing is working and doing classes at the same time. I think most people don't do that. I did that throughout all of college, but like working like part-time, like 10 hours a week or something like that. I think I could have done college or I could have worked. That's really what it is at the end of the day is...

Also for most of college I had a very committed relationship long distance, but we flew to each other a lot. I was juggling a lot of things and I think I just ultimately decided that my work is more important to me than finishing a bachelor's degree and going to grad school. Not because of the work per se, although I do care about it, but more like

financial independence and being able to you know live and not like be asking people for help is a big part of my my ego and dignity i guess yeah and i'll say what you're not saying school is a bunch of bullshit you know like um it sucks you have to do such stupid things yeah it's just the thing is the bullshit of it is the work doesn't get faster if you already know it

All right. This is this is exactly the thing is I go in knowing it by heart. I could teach the class for some of the classes, not all of them. But the homework is these these menial tasks that are very I mean, maybe it takes more time if you really don't know the material at all. But it's it's certainly not zero.

you know, even if you already know it all, just going through the motions, you know. So Zybooks, all right, tips for everyone out there. Zybooks, you can use key commands to get through it really quickly. You get the answers correct as long as you select them at least once because multiple choice. So you can use your arrow keys to like select all of them super fast and then tab to go to the next set. So you can get like lightning fast at going through Zybooks without reading any other questions.

Wait, what is iBooks? I don't know that. iBooks is the undergrad CS education platform right now. At least in California, but I believe outside of California as well. It is super duper prevalent and it is multiple choice questions that you can

get basically 100% as long as you do all of it. I see, I see, I see. Just to make sure that you're thinking through them, right? You're not just skipping. But even like, it'll still take, well, I don't know, at least a half hour to go through Visay books if you already know all the material and you're not reading any of it.

Like there's a lot of questions. It's really helpful. Okay. If you don't know the material. So like, obviously read what you think you need and don't just like not know anything in your class and fail on your tests, obviously, but like, you know, have judgment. That's the thing. I wish the professors let us decide how we prepare for tests. So if something is just super, like you got that in the bag, you can just not think about it and focus on the things that you actually need to practice.

That's the thing. Maybe we shouldn't make it publicly available that it's possible to just keep that fast. Otherwise, they're just going to patch it.

I think it's intentional because they put like work into making the tab and arrows work so well. There's like an there's some kind of version of you Ryan who's working on Zybooks and is like, you know what, I better, you know, spend a week implementing the tab feature to be really fast. Just for my it's like a backdoor. Yeah. This is Zybooks security backdoor.

I really resonate with what you're speaking about dropping out, right? Because in a sense, not in a sense, I definitely also dropped out by PhD and I mastered out, right? It's the equivalent of dropping the PhD in the US. And it's still, I don't know for you, but for me, it still felt like a failure, right? It's going through that decision process of being like, okay, I'm done. I don't have it anymore. Like what I...

what I wanted out of this, I kind of got. Things are not working anymore. I'm not satisfied. I'm not happy. What am I doing with my life, right? And it's definitely not an easy decision by no means. And you also have to weigh in the factor of, well, okay, what do I want for my future, right? Like how does this change things? And I'm curious because back in the day,

I would say it was kind of easier to become a software developer, you know, like be hired by a good company without not having a degree, without having a diploma. How do you find that nowadays? Are you still in the same company? Have you been out in the job marketing again? How was that? I've been pretty lucky.

because I know people, I guess. And this is the thing about working in startups is it's much more about like knowing the people as they're making the startups. And then you can kind of talk about like becoming a part of it. So this is definitely one of my privileges is, you know, my dad is in computer science and he, you know, he knows these people and whatever. And he's been able to connect me to people who are starting companies.

That's not the only way that I've gotten interviews. But at the same time, like, if that's how my resume was built, you know, it's still something you got to take into account as an advantage I have, you know, and I think nowadays, like you said, you don't need a degree too much, depending on where you go, some places you definitely do. But

What replaces that is work experience, right? And having, you know, like, oh, that tech came out last year. Well, we need 10 years of that experience or whatever it is. You've seen it. We've all seen it. And it's such a chicken and egg problem, right? Because like, you know, fine, you don't need a degree, but you need work experience to work here. But you need work experience to work anywhere. So you can't get work experience. So it's like, you're stuck, right? There's just nothing.

And a degree is definitely really helpful for that, I think, if you don't have other ways to get work experience. I think the industry is also built around unpaid labor in the sense of doing internships during your undergrad as a way to get work experience. These days, they're well paid. They're definitely well paid these days. A lot of the undergrad ones aren't. Really? I've never seen those. What a scam.

Back when I looked, internships were generally unpaid. I did an unpaid internship in high school. That's the only way they were going to hire me because I wasn't even in college yet. That and open source is also a big, giant, unpaid exploitation.

I will say though, I know plenty of people who graduate with a degree and still struggle in the job market for a long time after that. It seems like work experience is much more important than a degree. It's just, you know, when you have nothing on your resume, anything counts. So a degree is still helpful. So tell us more about your work experience itself. I started with JavaScript because that's just the first language I learned. And I got pretty good at JavaScript.

Do you like JavaScript? This is a type theory for our podcast. I must ask this. Do you like TypeScript? No, I do not. You can say you do. It's fine.

No, no. All the stupid bugs you hear people joking about on Twitter. You know, the the the Watt, W-A-T-T, whatever. Oh, my God. That's the best CS talk ever. Oh, yeah. We shared it around work. I've experienced most of those in the wild on accident. Really? And you're like, what?

It's crazy. I remember I lost a day or two to the fact that if you want to check if something is not a number, NAN, you have to check if it's equal to itself. Because NAN is not equal to anything, including itself.

So if you check x equals nan, that's not going to work. Nan will still be false for that. But if you do x not equals x, that's only true for nan. So that's how you check. This is in Mozilla Docs for JavaScript. This is the official way.

Is that the same thing in a TypeScript? Cause I thought like, I mean, kind of the, the big problem with all those in the Watt talk is that, uh, you have this crazy type conversion happening under the, behind the scenes and maybe TypeScript addresses that. I would, I would guess some of them. No. Okay. So TypeScript is amusingly unsound, like quite unsound. Um, like for example, uh,

If you index from a list in JavaScript, then it could be a value in the list or it could be undefined if there's nothing there. The types in TypeScript say a list of T indexing will give you a T, even though it's a T or an undefined. So it's like the whole point of types that we love in functional programming is maybe you have to handle the none case.

And TypeScript doesn't force you to deal with that at all because they wanted it to be more ergonomic and what JavaScript developers like. And that's just one example. There's a lot of famous examples of just the types being unhelpful with these kinds of edge cases. But these kinds of edge cases are exactly what we don't like about JavaScript, right? So, yeah, I'm pretty sure, I mean, TypeScript compiles to JavaScript and runs as JavaScript. So I'm pretty sure all the NAND stuff is still the same.

Could be wrong. Is Wasm WebAssembly going to be our saving grace for that, do you think? Or are we doomed to TypeScript slash JavaScript? I'm pretty Wasm optimistic, I would say. I like that you can write your front-end code in Rust. That's pretty cool. Something with an actually good type system. I think it has more growing to do.

And I also think some of the direction is kind of interesting. Like a lot of the most recent proposals that are going to get merged in are quite heavy. And like Wasm is not that lightweight anymore. Like they're getting a like ML style module system and a garbage collector. And it's like, I don't know. It's not really the little bytecode runtime that I got excited about in the beginning, I guess.

But maybe that's because I feel like languages that target it should be implementing those things themselves. You're just mad because you don't get to feel pretentious because you use Rust and you can avoid all these memory safety bugs. And now there's a garbage collector. You don't get that excuse. I don't know. What do you think? So you're saying simultaneously that WebAssembly is like underdeveloped, but also overdeveloped.

Is it like you would steer it in a different direction? What do you think it's missing still? The number one thing that I got excited about is their... So WebAssembly has a really weird control flow stuff. They don't have jumps. They have structured control flow, like if and while instead in the bytecode.

which sucks if you want to do a continuation passing style compilation to Wasm, which is like kind of too low level for that. This is the same problem if you try to compile to LLVMIR, is kind of too high level for CPS, which is kind of hilarious. So they recently added, maybe not that recently anymore, I don't know.

tail call instruction. And I think that solves the last problem that I was really worried about. I stopped paying attention before that was actually publicly available. I'm sure that's publicly available now. I think most of the development I would care about now is more like ecosystem stuff, but I also am not tuned into the community.

So yeah, maybe it's caught up. I have no idea. Tell us about your work and then we come back about the projects that you were working on. So JavaScript. I do JavaScript. All right. I did JavaScript. I've escaped recently into Elixir kind of hilariously. But I did JavaScript for a long time. I did not really browser stuff, more like embedded like

I used to work on this Mac app, but they wanted to add a Windows version at some point of the app. So they were trying to replace all the components in the app with little like Safari kind of widgets, like just normal UI stuff, but implemented in JavaScript instead so that you could do it in Windows as well. So that was a lot of my work for a while. And that was kind of fun, to be honest. I will say this about WebDev.

is it's really, really satisfying when you have this really pretty professional looking UI in front of you that you built. You know, I would spend hours just tweaking CSS numbers, you know, just pure perfectionism, getting it to look just right. And it feels really good. I'm just going to say.

But all that said, I'm happy to have been hired by a company that, I mean, they hired me for JavaScript, but then they decided to hard pivot into Elixir. And I'm like, an entry point into a functional programming job, you know, descends from the skies upon me. It's so good. So you already had experience with functional programming before that? Yes. Yeah.

Not really any Elixir experience. I think I had written maybe like, I hope my boss doesn't hear this, like 400 lines of Elixir before that. But I definitely played it up a little, which is fine if he hears it. Cause like I've written a lot at the company now. So I think I've proven that I figured it out. But I wrote a lot of Haskell. I'm a Haskell guy. I've never learned Okamo to be honest. I know that's, that's going to be crazy for some people. But yeah,

I learned some functional programming from Java, hilariously, and JavaScript. And I thought this was pretty cool. And I heard the Lovecraftian tales of Haskell. And just this archaic...

incomprehensible madness that is apparently just pure magic and i was like all right well you know i gotta learn it right and this is the same with category theory around the same time it's like this is impenetrable so i i need to learn it even more you know and find some kind of entry point which was not going to be wikipedia or anything else that's just maximum impenetrable uh

And I don't remember exactly how I finally learned it. I think I literally just scoured until I found some helpful blog posts, which is kind of the story of my life and why I write blog posts now. And I got a lot from...

the very famous popular Bartosz Maluski on YouTube. Oh, yeah. Category theory lectures are... I cannot recommend them highly enough. I really learned a lot from that. So I got into Haskell and functional programming like that and Lambda Calculus and...

that was again, kind of all in my own time, but with the help of other people, um, discord communities and whatnot, Reddit. And that's really changed everything about how I code now. And the fact that I, uh, that the company I was already working at was switching to Elixir was very, very exciting for me from JavaScript of all things. Right. Uh,

which was really like TypeScript and React. And now we do a kind of Phoenix live app, which is very strange, but I've learned a lot about web development and frameworks and whatnot.

and started working on my own for my website, which is very over-engineered. And I made sure it was extremely performant before this podcast so I could show it off if anyone looks. It does look really good. I don't know if I access before your update, but it's really good. It's been fast for months, but now it's a little faster.

Yeah, which is all just build time. So the secret is it's a compiler, right? Any project I work on, it's a compiler somehow, right? And so I write all the posts in a markup language and compile it all to JavaScript and HTML and then serve it statically. So that is the highest performance you can get. And some frameworks are switching to that nowadays, like Next.js does some of that in Astro.

But I just do it because it's a compiler. And you know, it does the whole parser combinators and all that, you know, the classic toy language story. It's great. It's a lot of fun to hack on. Yeah. And I took all that tech and published it as a framework called Arctic. But I think I'm still the only one who uses it.

Well, now it's a great opportunity to advertise. It's going to be in the link in the description of the show with all the links and people can check it out. Maybe someone will think it's pretty cool. And then you use, I remember correctly, you use like Gleam, like this language to doing that? Gleam as in shiny. And I think a lot of

people in the kind of self-teaching PL space know about Gleam now because it's such a young language and usually the first people to use young languages are these PL folk. So I came to it pretty early for exactly that reason. But they got really popular, I guess a year ago now.

when they did their V1 announcement and Primogen and Theo did YouTube videos on it, which is like, that's a big deal in our little space online. No Fireship video yet, but the logo did appear in a Fireship video about Erlang because Gleam runs on the Beam, which is kind of exciting, but it also runs on JavaScript.

It compiles to both and you have to specify your compilation target in your code, but you can have code that's agnostic. So you kind of have your project structured in this like top level, I don't care, define the data types. And then you have a code that ends up on your client and code that ends up on your server.

And the client stuff, it feels a lot like Elm, which is a language that I liked a lot. Very Haskell-like model view controller compiles to JavaScript. It's a nice way to write websites, front ends. I like it a lot. And then the back end compiles to Erlang, and you get everything nice about the Beam and concurrency. I know Dan knows a lot about that. It's exciting stuff.

So I'm a fan. I mean, the thing that it's most famous for right now is extremely, I guess, minimalistic language design principles. Like they're not going to add pretty much anything anymore.

And there's no if statements. You got to do a case statement on true and false. It's like, really, there's only one way to do anything in the language. And I like it a lot because everyone writes it exactly the same way. And it's the most readable. It's a lot like Go in that way. And people talk about it like a Go for the beam or a functional Go or something like that.

Besides that, it's, you know, Hindley Milner, very standard kind of functional language. But it has Rust syntax, curly braces and parentheses for calling functions. And I really like it. Yeah, I'm a fan. Can't talk about it highly enough.

And also because I built a little bit of the ecosystem, like one of the Parse Recombinator libraries. And I just feel included. I mean, it's really famous for the community and just really friendly people, as long as you're a leftist, pretty much. But yeah, really friendly people. Yeah, yeah. It's, you know, like very queer, I would say. Yeah.

Yeah, a lot of LGBTQ representation, especially trans. What accounts for that? Is they have like a keyword for that or something? I think the main thing is the website is pink and says no Nazis on it or something like that. And it's just the BDFL, Beneficial Dictator for Life.

is Louis Pilfold. He's a super sweet guy, but also just very forward about his politics. So it's nothing about the language per se, but just the kind of community that he has fostered. But I happen to be leftist and liking of queer stuff. So it's nice for me. And I think it's great. Honestly, I can't stand any of the other stuff.

I was honestly thinking about like adding, I feel like the future of technology is to add stuff like that to the licensing of, of software. I, I played around a little bit with the idea of, um,

There's something called a Hippocratic license. I don't know if I've talked about this on a podcast before, but I think it's really cool. It's this idea. It's like an MIT license, but it says also like you if you're a government and you're using this to, you know, in the police software or something that you're you're not supposed to.

you know, well, we would see if that actually gets used, you know, but I, I, I look through, they have, you know, how many pieces of software actually use this, this license. And it's just like,

some, some Python video games or something like that. So I don't think the police are going to use it, but I think it seems like, why is nobody talking about this? Why is nobody using it? If you look it up, you'll see like a lot of discussion about like the V1 version of that license, which was like too vague. I, I like what they're doing with the Gleam community from the sound of it. And that makes me think about the,

how I feel like the future of kind of open source software is to have more, to increase the amount that we start to care about these types of things, like what our community is. Yeah, I mean, I know that there's like codes of conduct, for example, but one of the things that

My, my fiance got me to think about was that like I so I was writing like a piece of software and I was telling her about it and she said, Well, you know, if so you're going to open source it so what happens if like you know it goes goes into a drone and it's used to like murder somebody.

And I'm like, you know, we don't care about that. And then I heard the words coming out of my mouth while I was saying that. I was like, this seems kind of wrong. But initially, like, I really kind of fought against her for this. I thought, you know, I'm an open source kind of guy. I was more of a libertarian back then. But, you know, through talking to, like, actual humans, I

I've gotten more of a sense of like, I feel like it would be useful to encode somehow the, like the values of the community. So I was looking at like the Hippocratic license, which if you Google it, the first thing you'll get is like a hacker news article. This is a very long, long tangent, but you'll get a hacker news article. That's like criticizing the version one of the license, which was like a,

a little bit kind of naive and vague, but then they got like an actual lawyer to vet it. And they have this version too. And it seems actually, I mean,

It seems like it holds water, although it's never been really tested. If you look at what projects use this Hippocratic license, it's just like a bunch of like Python games or something like that. But I think it would be really valuable for people to try out this license that basically says, for example, and you can pick whatever you want. You can say if you have a problem with the police, you can say, you know, this this software should not be used in kind of in police software or something like that.

And then, you know, eventually maybe they will use the software and then you have to sue them and you get to enjoy that. But I think it would be cool to try that sort of thing. I like that it's working in Gleam. Of course, the tradeoff is that if we're going to get like nice leftist software, it means that we're also going to start getting Nazi software, which already exists. Oh, yeah, it does. Never mind. Then, of course, the Nazis are ahead of the game in that area.

But yeah, I feel like it's cool. I don't know. What do you think? Am I being naive about this? The licensing thing? I was thinking here in my head that I was actually reading something along these lines today. And I kind of relate to what you're saying about this discussion you were having with your girlfriend, right?

My fiance. Sorry, your fiance, Mimi. And, you know, I kind of relate to that because... And I think I understand a little better why I feel a little...

I don't want to say that I'm against any of that, but I felt a little weird bringing this discussion to the table. And I didn't understand exactly why I felt weird. And I'm reading this book by Richard Feynman, The Meaning of It All, and he brings it up, this discussion.

that those are actually two separate problems, right? There is the scientific endeavor by itself where we're trying to fuck around and find out things in nature, right? Like we're just poking at bits and bytes and whatever and trying to figure out what is going on. That's problem number one and that's science. But then what are we going to do with it? Well, we're going to... It brings power. We can do more stuff. But...

it can be good or bad stuff, right? And where do we draw the line, whether it's good stuff or bad stuff that we're going to be doing? But here's the catch, though. And I finally understood why it made me a little weird is because this is now a second problem, right? This is now a...

a humanistic problem where maybe it's not even the scientists themselves, us, that it has the best tools to figure that answer out, right? Like my job is to make the discoveries and I don't know, maybe I'm being a little selfish, but I feel like

it's better for someone who understands better the nature of human societies and what people want and how things are engaged to figure out, okay, how is this going to be better used? Right. But I don't know. This is me. Like, I feel like, you

you know like science itself is just poking with nature and things and and what we're gonna do about it that's the second problem already but um i i do not i don't want to take away the responsibility of you know like these are important problems to discuss you know like what should we be doing with that and and like this these licenses and for sure you know like everything relates

works around communities, you know, like programming languages are communities oriented. And even, even there's this podcast where we're growing a community of people who thinks around similar topics. So it makes sense to like, everything's political. Everything we do is political.

is kind of political, right? And it's nice to have a language that from the ground up is, you know, like take those values into considerations. But I also think at the same time that it's important to keep the distinction that these are two separate problems, right? Yeah, I think that's the principal kind of reaction that people have to something like that. You would see the analogy of if you're making a nail,

you don't, you, the nail doesn't come with like a little license that says like, you shall not use, or a hammer maybe as a better example, you shall not use the hammer to, to make a bomb or something.

And I think that that sounds like pretty persuasive. But if I was like a hammer salesman and a guy like comes in covered in blood or he's about to be covered in blood, he says, like, I'm going to use this hammer to like kill my wife. I'd be like, no, I'm not going to give you I'm not going to sell you the hammer, dude. Like so there is some apparently to me, there's some kind of component.

at some point where I do somehow get involved. And yeah, it's a weird line for sure. I would like to see more discussion about it. I think that, I don't know, maybe with Trump, with the current presidency, maybe that discussion will be postponed, but I think maybe eventually it will happen. What do you think, Ryan? I have two thoughts on this. I guess one is, first of all, like we're

We should realize that we're really talking about the open source community, not the research community. And most of these projects are not doing novel research. I'm 100% on board for the pursuit of knowledge, advancement of knowledge in math and computer science. But for example, Gleam, or take your average programming language nowadays, is not trying to do that. They're not publishing papers or anything. It's just a project to help people build things.

And that's most of open source. And I guess-- so that, first of all, places it firmly in your second problem, Pedro, of just the humanistic. And I guess I feel like-- I mean, you kind of said this, but I want to hammer it home, so to speak.

If you are doing something humanistic and you're trying to be apolitical about it, you are being centrist, right? Whatever the middle of the Overton window is, right? And in the US, that's quite right wing.

Right. The truth of the matter is that that means, you know, the the all the cops stuff. Right. Cops is our running example, I guess, is, you know, you're pretty on board with that. Right. If you're if you're not saying anything. Right. That's the truth of the matter. Right. The bystander issue. Right.

So I think it is quite important to take a stand unless you really are happy about the current state of the country or whatever. That's how I feel. Well, I'm glad we didn't go too much into Trump or Nazi anymore. Don't want to be canceled on my first video podcast.

It's an important conversation to have. That's what I was going to say. You know, like there is a lot of news and stuff coming up for those who are going to be watching this in the future. This is like early February and Trump has, I almost called him Trump. And Trump has been, you know, like just...

shooting a huge amount of orders through the White House and I think he has cut NSF funding and are deporting a bunch of immigrants and you know like there's news about Brazilian people being handed in airplanes with these horrible conditions and things are really weird right now and it's

an exciting moment in human history to be alive. Everything is just, you know, like so upside down. But, um, yeah, these are definitely important conversations to be having, but, you know, let's come back for a second now and talk about, um, types, type theory, exciting projects, and, um,

We were talking about Clean and how you dropped out of your college studies. Let's talk a little more now about your projects. I know Dan is really, really excited to hear about Saber, Saber VM. Tell us about the history, how these things came about, what you were going on in your mind to bring those ideas to mind and what they are. Well, okay. So one of the...

So a lot of people getting into programming languages, self-taught, will read something called Crafting Interpreters. I did not read this, but there's a very similar book that is also quite popular called Writing an Interpreter in Go. And I did work through that because I like to go quite a lot. And it has a follow up, Writing a Compiler in Go.

And that was very exciting to me because, you know, as we all know, compilers are strictly better than interpreters all the time. So that's a joke. We don't know that. But that was exciting and it was not that difficult. It was a bytecode compiler, though. And, you know, I have a tendency of building something that I think is cool and unbelievable and immediately thinking it is not cool and unbelievable and moving the goalposts further.

So I ended up with Compiling with Continuations. It's a book that I cannot recommend enough for compiling functional languages. And it does go all the way to a kind of assembly generation at the end. But it uses continuation passing style very heavily throughout the book. Who... Andrew Appel. Yeah.

Yes. Blanking on the name, but yes, the, the SML New Jersey guy. Is there like a more recent version that's in, in Java or something? Or is it, was it written in SML or OCaml? You're thinking of...

something else. You're thinking of the Tiger book, I want to say. There's some other book that has one of the versions are in Java. But compiling with continuations is an SML, which I don't use SML. I just did it in Haskell or something, but it's close enough. And I got really excited with continuations because they're crazy powerful. And somewhere along the way,

I was listening to Type Theory for All podcast and learning about classical logic from Cody Roo and continuations and all that. And so I don't know, there's something very aesthetic about all of that for me. And the thing is, we kind of touched on this earlier. If you use continuations as the way to implement your functional language, then you're

I mean, first of all, it's great because it's just jumps. So it's very performant and you don't have a call stack and whatever. But you can't really use LLVM. You can't really use Wasm, right? The world is built for imperative languages that are just not doing CPS, right? And so I thought, well, you know,

CPS is lower level than these things, right? It's strictly easier. It's just a go-to, right? At the end of the day. And so I started working on Saber VM, which is a typed VM based on a lot of things that I was excited about around that time, especially research by...

Greg Morissette. So it is like memory safe using some of the stuff that inspired Rust's borrow checker, but it's not like substructural. You can mention things as many times as you want. And I like that a lot. So that's a calculus of capabilities. If anyone wants to look into that, I'm a fan of that line of work and it is typed using again, Greg Morissette's typed assembly language research. I'm a big fan of him.

And so the type checker is in Rust, and it just turns bytecode into kind of untyped bytecode, hands it off to C, and runs it in the usual fetch eval loop of a bytecode. And it was pretty fast. I got it to work fine.

I didn't implement all of the things that I wanted before kind of moving on to something else. But I got all the memory safety stuff working. I wrote a compiler that targets it from Lambda Cataclysm in Haskell. And that all made me very happy. I was exploring kind of some concatenative stuff at the time. And it's a bytecode language. So that was a trivial compiler to write as well.

I think this area is awesome. I love the ongoing exploration of memory safety without a garbage collector. So this was kind of arena-based, I guess you would say, as you allocate these big chunks of memory. And then you can freely allocate in and out of those as long as nothing lives longer than the arena itself. And then you just free it all in one go. And that's awesome, I think.

People who've explored a lot more of the low-level stuff get excited about these kinds of things. Since then, I've hated garbage collectors less, I'll be honest, which I've heard is common. But the low-level community has its own kind of self-teaching community called the Handmade Network.

that I just wanted to take a moment to shout out because they're super helpful and great about all of this. This is like Casey Muratori, Ryan Fleury. I got into that because of Randy, the YouTuber, Game Dev. That was fun. I liked his stuff a lot. And yeah, so all of that paired with the papers I was reading by Greg Morissette turned into Saber VM. And I'm probably going to come back to it and keep adding things to it over time. It's a pretty cool project. I think we need more targets for continuation passing style.

So do you have continuations in the type system? Is it a specific type, or do you have functions at the assembly level? What's going on there? So this language comes after hoisting, so there's no lambdas. It comes after continuation passing style conversion, after closure conversion, which means there's also existential types. So it's...

It's pretty much just the last type system in Greg Morissette's very famous System F to Typed Assembly Language paper that's like 70 pages of like, I don't know, a lot of pages on like transitioning between different type systems. And the continuation type system thing is very simple because it's a function type that just has a left side and no right side. And there's no...

It's all hoisted out. So it's just the labels to jump to functions at some point that have those types.

and then the type signatures on blocks of code themselves. So if we had listeners who wanted to write their first continuation passing style compiler, is Saber VM ready to be a target for something like that? I know that you've already made one language based on that, but I'm wondering to what extent do you think other people are ready for it? I mean, I know this is-- the expectations are low. This is a hobby project. The fact that you did anything at all is miraculous.

I'm just curious. The main disappointment I have with it, that's roughly where I stopped working, is I really care about asynchronous IO. I hate the idea that writing to a file is going to block the whole program. And that's pretty hard to do because it's just a C runtime, I guess. And I was somewhere along the way in figuring out how to do that and just kind of got demotivated and burnt out.

So it doesn't have that, and that makes me sad. But for a fun kind of baby's first continuation passing style compiler, I think the most annoying part... Actually, I don't know. How does it compare to if I targeted x86? The problem with targeting x86 is it's so complicated, and then you have to deal with whatever assembler. It is mostly very easy.

and a great project. And I have that compiler public on GitHub. I have pretty much all my projects public on GitHub in case people look at them. And people do. I also write very readable Haskell. That's a rare thing. I don't use 99% of the features. I don't use custom operators. So yeah.

Everybody thinks they write readable Haskell, except maybe Edward Kmet. The Haskell people I've talked to don't like how I write Haskell. I'll just say that. Do you use monads at all? It's very verbose. Yes, you should know how monads work first. But I usually use one monad where I define all the effects like IO and exceptions and state. And then I don't use transformers or anything like that.

Oh, at that point you should be just using OCaml then. That's how you do monads in OCaml. I haven't learned OCaml. I haven't gotten around to it. I hate how it looks syntactically. I keep getting scared away, but I should learn it. To be entirely honest, from what you're describing, I think you would find OCaml a better home for your style.

Sounds likely. I write gleam in exactly the same way. Gleam has a use keyword, which Rock, not the proof assistant, also has called backpassing. And it's like a let binder that gets the scope as a continuation that you can pass in. It gets passed into the value.

and it kind of replaces do notation. So there's no monads, there's no type classes, but you still have what looks very much like do notation.

And I use a lot of do notation in my Haskell, I will admit. And so gleam, I think, is written very much the same way, but just without ever having to explain what a monad is ever, which is great. It's very simple because monads actually are very simple, and it's just bad terminology. And related to continuation. No, I mean, the online monad tutorial is so like--

infamous, I guess. I didn't want to go near-- I actually do have a Monad tutorial, but it's just the category theory. And I say at the top, please don't use this as a Monad tutorial. We're already full of Monad tutorials at this point. Yeah, I did not want to touch any of that.

But I think they are pretty easy and just poorly explained. And I mean, you want to learn how a monad works, just use it. Just use it a bunch. Figure out what's not working. Actually implement the stuff.

It's like I was saying before with lots of small projects. I think you just have to implement everything you learn about in some little way. And that's just how you know if you understand it or not. FRANCESC CAMPOY: And honestly, this is something that I'm seeing right now. I'm trying to learn this research language

SAPIC Plus and Tamarin where you can do some protocol verification style stuff. And it's really going over my head. It's like, it's hard to get aggressive because it's a whole new thing. It's a whole new paradigm, right? And I've been struggling for like

a week now and I finally decided, okay, let's sit down and just write something, whatever. And in these last three days that I sat down to actually write something, I'm learning a lot more than the rest of the three weeks that I was just reading stuff. So like sitting your ass and doing the work and actually getting something to compile, getting something to run and just messing around with things often get you

much further along. So yeah, I definitely agree. That's pretty cool stuff. And that segues nicely back to SaberVM, which is that this is my first Rust project. And I think Rust is the exception to what we're talking about here because... You have to learn a lot first. So hard to get something to work in Rust first try. I mean, my first project was a long time before that actually trying to do just a basic like Lambda calculus thing.

just evaluator, I guess something really simple. And it's like, no, like trees and like, you don't know lifetimes of what things are. It's like, it's miserable. I now know how to do that pretty easily in Rust. But I just remember feeling like this really easy task, even easy in C is like way too hard in Rust.

And SaberVM, I came back to it because, again, I've been reading a bunch of Greg Morissette. I actually found that learning the theory from the papers and like substructural stuff made me totally understand all of the rules and rest. And I was like, oh, like that actually makes perfect sense. I know exactly why. Like, I can't do it this way. It's because I'm, you know, carrying around multiple mutable references or something. That's a no-no, right? It's...

So that was the one case where reading a bunch of papers first made me actually able to implement something. And then using Rust was a dream for that. I use clone a lot, I will admit. So I'm not like a hyper-optimized Rust programmer, but I at least can build things and do build things. And that's new. That's exciting. Yeah.

Yeah. Oh, and to answer the question, the one thing that's different about targeting Saber VM is the way it does memory safety. You need this kind of pass to allocate everything into arenas, kind of a region inference stuff. But once you have everything in CPS, putting it into stack-based bytecode CPS that is Saber VM is like,

just a dream. It is so, it's almost trivial, you know, you just kind of plop in the tree and you're at the AST in like,

like Polish notation, basically. Right. I think I should have asked this one question much earlier, but I think some audience will still appreciate it. But could you explain very simply, maybe Eli5, what is continuation passing style? Sure, sure. I mean, my thought process is that it's been talked about on the podcast a fair amount because that is where I learned a lot about it. But continuation passing style is

is where functions don't return things. They take as a parameter a function, and they call that function with whatever they would return. So it's kind of like you tell it explicitly where to jump to when you're done, right, with your return value as one of the parameters. And that means...

Well, one thing is just a kind of illustrative example. Continuation passing style doesn't have like laziness or strictness or whatever, right? Because you just specify at every moment what the next thing to do is, right? So you can compile lazy to CPS and you can compile strict to CPS. And there's two different like,

evaluation, like translation passes to do that. Because everything is explicit, you can just implement it in it lazily or not. And that really is the value is it makes all the control flow very explicit. And you never return from a function, you just go to the next function, which means you don't need a call stack.

because the purpose of a call stack is for when you're done with a function and you come back to the caller, but you're never going to come back from the caller. So you can just forget all of that information right on top of it, free it basically. I mean, not literally, it's more complicated than that, but it's a jump. That's the punchline. Calling a function becomes a jump, even a recursive function.

So recursive functions compile to while loops. We love that, right? Because it's just go-tos at the end of the day. And it has that benefit as you call functions a lot in a functional language, obviously. And we really want the bytecode, or I should say the assembly, to look like if we had written C instead or something like that.

And CPS is one good way to do that. It is not so popular nowadays. Things like ANF. ANF is more popular, I've heard. Administrative normal form is, I believe, still has to have a call stack. But I'm kind of talking out of my butt at this point. So I won't say too much more about it.

just a different IR that has different advantages and disadvantages for manipulating it. The main thing people don't like about CPS is it's like a giant whole program transformation, very extensive. And so a lot of other IRs that try to be better than CPS, usually they're just closer to the source code you wrote. It's just less effort to put it in that form than it is to put it into CPS.

But once you're in CPS, I mean, there's a ton of research on optimization. Like I learned a lot of optimization again from that compiling with continuations book, which has just a lot of examples that was really helpful for me to learn. And it's all done in CPS as the IR. So it's quite well studied and good for performance. It's just longer compile times.

I think this is a good moment for us to shift towards learning resources in PL and type theory. Unless then do you have any other more technical questions over projects and concepts? Yeah, well, I thought it was really interesting that you were using the Beam virtual machine in some kind of project. And I was wondering if you could maybe tell some of us. I mean, I've worked on actors and stuff.

but I actually don't know kind of what are the advantages really of using Beam Virtual Machine. And for people who don't know, that's like Beam is to Erlang, Elixir, and Gleam what the JVM is to Java, Scala, and Kotlin. So it's this virtual machine, but there's some kind of special properties. People talk about it as if it has some kind of special fault tolerance properties or something. So I thought maybe you could tell us a little bit about that.

Well, one interesting thing about the Beam is Java, Kotlin, and Scala are three very different languages from each other. But Gleam, Erlang, and Elixir are quite similar to each other. And the thing is that the Beam only supports functional immutable languages.

which is kind of a big surprise for people. It's also, I believe, pretty CPS-oriented. I don't know too much about that, but you do use these kinds of... They're doing something that's similar and doesn't have a call stack, is what I seem to remember, because people were talking about compiling Elixir to Osm and saying that you couldn't do it for all the reasons I was talking about before. So...

That's one thing. They do the immutable functional stuff because they like immutability and they like immutability because the beam is extremely concurrent. That's kind of its big thing. The value add, I would say, is it's it you spin up processes just kind of trivially. It's kind of like go like that. You just you just spin them up. They're very, very lightweight in terms of memory and everything.

And there's a good scheduler that organizes it all for you quite nicely. So there's a built-in notion of like a process or an actor, basically. Yes. Yes, exactly. And I'll be honest, I find actors really hard. I don't actually use them that much, just conceptually. But this is something that people like about it. Another thing people really like about it is introspection.

Like you can see what the state of the runtime is as it's running and kind of muck around with it, like a live coding almost kind of thing. And that's, you know, because the Beam explicitly supports that. That's kind of a hard thing to support. They even have hot code reloading where like you can update some parts of the program and it will just keep running alongside older parts that you're not updating. And these pieces just...

connect magically. Because of all of this, it's also generally untyped. Elixir and Erlang are untyped. Gleam is typed, which means they don't support hot code reloading. That's kind of a big deal. You can't actually do all the beam things in Gleam because it's not typable.

Or maybe if it was dependent types or something, you could do it. But Gleam just decides hot code reloading is something you mostly care about as a telecom company, which is what made the Beam. Most people don't care, don't really use it. I don't know. I used Gleam quite successfully. Again, Gleam compiles to the Beam and JavaScript.

And so the main way I use it is this kind of full stack approach. I think most people use it. It's very much a web dev language. So the process notion we talked about in the Beam is very popular for web servers. That's kind of the big thing outside of telecom that it's used for.

You can't really write a game like a desktop GUI app in the Beam. I mean, people have tried, so I'm told, but it's just not really made for that. But it's very, very good for web servers. I don't really use the Beam stuff too much in my personal projects. I got...

I fell in love with Gleam. I found Gleam because I wanted to learn more about the Beam. And it's the typed language. But I just love Gleam. And it became, I would say, my favorite language. And so I just make things in it now. But I usually compile them to JavaScript. That way, I can show them off on my website, for example. So it's very shareable like that.

There's a fun video from a Twitch streamer, Tsoding, T-S-O-D-I-N-G, where he goes into the Beam live. I only saw a little bit of it, but it seemed like a really fun video. I wonder if the Beam has anything to do with the Chicago Beam. I think Beam was made by Ericsson, which is-- where are they from? Are they British? Oh.

For some reason, I thought they were Scandinavian. The name is very Scandinavian, but I believe all the beam work happened in the UK. Yeah, maybe it's a Scandinavian company. Actually, I have no idea. Joe Armstrong, one of the big guys behind that, and I think Robert Erding, they're British computer scientists or programmers. Yeah, the work I paid attention to was happening in the UK, that much at least.

I don't just use the Beam in personal projects, though, because, again, I'm a full-time Elixir developer now. So I actually do have to use an actual web server back end proper gleam code stuff at work a lot. And that's kind of interesting.

Elixir is a weird language, got to be honest, mostly because of the metaprogramming that is just kind of everywhere in the air you breathe, I guess. Because Elixir doesn't really have the core things you would expect, like if statements. Those are all defined with metaprogramming so that it feels like they're there. It's a cool language. Yeah, it's a cool language. I mean, it has case statements, so hence you can implement if statements. But yeah.

But it's this kind of minimal language plus just a lot of metaprogramming that-- it's not like Rust metaprogramming where there's an exclamation point. It's like you can't know for sure if something is a macro or not just by looking at it. So it feels kind of weird and pervasive.

And there are patterns, obviously, right, in the community. It's conscious of all of this. But it's an interesting language. How long you've been using Elixir professionally? Professionally, started, I guess, in November. So not that long. Oh, OK. Yeah. Still getting used to it, probably. I don't know the ecosystem pretty well, but I'm quite comfortable with the language.

Elixir also has libraries for actors that are pretty friendly, I would say. Not needing types is something that ends up helping with that quite a lot. The gleam actors are a little bit scarier because you've got to type everything correctly. When I was playing around with Elixir, the very first thing that happened within an hour was I got into a very subtle type thing.

typing bug involving actors. So I would have liked probably Gleam a little bit better because it would have provided me that kind of foundation. But they also have some really exciting work in the Elixir type system, the set theoretic types. True. That's exciting. Yeah, I did see that. It's a lot like TypeScript in the sense of this is an untyped language and we're trying to add types to it at the end. And so you get intersections and unions like you have in TypeScript. It's a very...

extensional type system, Curry style. But it seems really cool and exciting. And there's genuinely novel research going into it and papers. And so, yeah. I don't think it's affected us too much. I don't remember seeing warnings about it. But I know some chunk of it is out now for Elixir developers. So that's cool. All right. Let's take this opportunity and shift gears. Let's talk about the resources.

that you have used for self-learning all of this content. I know you have a blog post explaining a lot of those things. The link for that will be in the description, but let's go through a couple of those. Sure.

One second as I pull up. Well, I guess I'm thinking, is it more helpful to go through the resources that I used to get into PL theory or to go through some of the things in this

in this post that are papers on interesting topics that not everyone has even heard of. Right. Let's start with the ones you've used and that you think it's useful to get kind of like started. And then we can even have a brief introduction of how to get yourself started with reading papers, right? And that will be useful for some of our audience. Sure. So I've mentioned some throughout the podcast episode already, obviously.

writing a compiler in Go. I loved it. Super accessibly written. That was one of the early ones for me. Bartosz Maluski for category theory. His lectures are fantastic. He is very funny and enjoyable and accessible. I've gotten a lot from emailing researchers when I don't understand their papers. People are very nice, and I don't think people do that often enough.

And, you know, if you can't access a paper because you're not in an institution like me, and even when I was in college, my college is not that research oriented, so I didn't really have access to things. And again, emailing professors and researchers is great. And they just give you these things. And people should not by no means use things like SciHub or LibGen at all, ever, ever. I'll just say that.

It's generally unnecessary. Like there's pretty much always some other way you can get it completely for free. Right. That's the thing. It's like, I haven't spent... Guys, do not use it. I'm telling you, don't. Do not go to libgen.whatever is the... Do not Google compiling with continuations PDF...

Right, yeah. Make sure to block that in your browser, okay? Use a block extension blocker. That's evil. Don't do that. You can get papers for free. That's bad, okay? Yes, all of that is good. And also, to be serious, it actually is pretty easy to get papers for free. Even if they cost a lot on one site, they're free on another site kind of thing. A lot of our publications...

And PL nowadays are completely free. Like SIGPLAN has put a lot of effort into making that

make sure that happens. It's a common thing for people to put their papers in archive these days as well. So we are in a very good place as a community in programming languages and even type theory. So yeah. Yep. Yep. I read from the ACM website and from archive quite frequently. And people link papers to each other to say like, oh, look at this cool thing, right? And they'll always like the one that's free pretty much. So it's like,

Yeah, like people talk about papers on Reddit as well. If you want like to learn about what is being studied right now, it gets linked as it's coming out. Learning logic. There's a YouTuber named Mark Jago. I really like he's very beginner friendly. He was just like first order logic stuff. If you didn't, if you're doing this before undergrad today.

Also, brilliant.org, not free, but their logic course was really good and I learned a lot from that. Really? Maybe I should contact them to sponsor the podcast because I've seen them sponsoring some science YouTubes. And I'm always curious, are these people being honest that this is good, right? I found some things useless, but the...

Machine learning and the logic were both quite helpful for me. And I got a little bit of value from data structures and algorithms, but not that much. Ryan, don't say any more until we get a sponsorship from them. They're not getting any free advertising from us.

I liked what in Dan Harmon's podcast, they started off trying to say really nice things about Nike to get a sponsorship. And then they started saying really bad things about Nike to say, we'll stop bad mouthing Nike if you finally sponsor us. So maybe we should do one of those things. All right. Yeah. Brilliant sucks until they sponsor. Yeah, pretty much.

Also, I have to mention Richard Southwell. I don't know British last name. I don't know how to pronounce those. But he's fantastic for dependent type theory, category theory. Curry Howard, hating algebras, which is where I learned sequent notation, is just fantastic.

I link him whenever I can to people because he is one of the most underrated resources in the community for sure. Um, so I will give you some way to link it, but it's also in the blog posts pretty much at the top for, for this reason. Um, uh, this podcast is a resource that I got a lot of value from. I learned a lot about Sadeel, which has become very exciting to me. And I almost have my own independent implementation of Sadeel. Yeah.

You're working together with Andrew, who you guys like in touch? He helps me with my dumb questions. It doesn't feel collaborative though. It feels like I'm bothering him. I'll bother him all you want. He's a very botherable person. I couldn't find his dissertation at all and he helped me find it and then he answers questions about it sometimes. He's super nice. I have a complete implementation except for maybe one off by one error in the De Bruijn indices and it's

driving me insane because it's stopping me from deriving induction, which is like the one exciting thing I want to do in Cedil. Were you able to dive into the weeds of the crystal spatially thesis deriving induction from those things? Because that was... It completely lost me, man. Like, that is really, really deep type theory hard stuff going on there. I find it really, really hard. So what I've been doing is...

Krista did the...

MARK MANDEL: You said they're the pretty face of Sadeel, right? Because of SadeelCast. That's been helpful for me because it's just an implementation of deriving induction in code. MARK MIRCHANDANI: Oh, yeah, yeah, yeah. There's that. MARK MIRCHANDANI: So I looked at the papers, the thesis, and I'm like, this is crazy and hard. But you can just do it, right? There's code examples online of doing it in Sadeel. And so I've pretty much been doing that

in my little implementation called Candle and got stuck because I've been off by one error, unfortunately. But I love Cedille. I think it's a great direction. The team is super nice. They're hilariously podcast-oriented with two episodes here and Aaron Stump's own podcast and Cedille cast and Aaron Stump on another podcast. Is Aaron still doing the type theory commute where he's in the car? Yeah.

He doesn't do it super frequently, but I listen every time. No, last time I checked, I think he has a better frequency than I do, but it's much shorter. Yes, that is true. But they're much shorter. And he's in a car. It's a resource that I would recommend. I listen to Iowa Type Theory Compute.

and definitely suggest people check that out. Reddit is r/programminglanguages. It's not really about programming languages that exist. It's more about programming languages that people are building and research coming out at Popple. And it is awesome. And the people there are super nice, unlike many subreddits. And they have a Discord server as well.

I don't remember. Like I, I was linked it from a friend. I don't know if it's on their Reddit page or not, but it's definitely an official discord that would not be hard to find and get into. And there's a ton of people talking about PL theory and helping each other at just every, I mean, every skill level. Like it's the most unbelievable thing where like some people will like decide they're going to tackle some crazy, like,

open research problem and in my head i'm like that's so crazy right that's an open research problem right you're not gonna solve that and it's like they solve it and it's like all right these are the same people that are writing the papers at popple every year right they're here they're here and doing their work in public which discord is this

This is, I mean, there's several, but the main one is a programming languages Discord server. Oh, I didn't know about that one. You have to send that to me. Easy to find from the Reddit. Similar is Mastodon. This is even more the case where like all the researchers that I love and read papers of are just on Mastodon talking about their research as they're doing it. And like,

Again, I'm a big Bartosz Maluski fanboy and I can just ask him questions there and he just responds to me like a normal human being and not the god that he is. And it's crazy, right?

It's unbelievable that they're just there, right? Just talking and being normal human beings. I think that was kind of my first reaction when I went to my first Popo conference and I met like Benjamin Pierce, Steve Zdencevich, Stephanie Wierich or Adam Szpala. And I was just like talking to them regularly. I was like, I want to meet them someday. I'm going to meet them someday. They better prepare. I'm coming.

No, that's the thing. Like our community is super, super chilled. Like everyone treats everyone super nicely. And it's, yeah, I was actually very surprised because I did not expect that from my academic background. Like the professors that I've met previous to programming languages community, they were kind of like,

they had an act on them. They're like, oh, you better respect me for who I am kind of thing. And that's not the case in programming languages at all. People here are very, very excited to be sharing their work and all. It's kind of against stereotypes. And it took me a long time to figure it out as well. There's this guy in the south of France, Luigi Licori. He did a row calculus, like a rewriting lambda calculus.

And I got interested in his research. And then I had some questions about it. And I emailed him. And this guy, such a lovely introduction to talking to researchers. He is so sweet. He is a puppy dog of a human being. He set up a Zoom and we talked together for a long time and just...

just his joy about everything. And he wasn't, this was a paper from 2004. He's been studying totally unrelated type theory for years now, right? He's on intersection types or something just really different from the rewriting stuff. And it was so much fun. Yeah. So I definitely have to just encourage people to just reach out to these researchers and just try. I've always had a good experience doing it.

But I think it's worth mentioning as well that, you know, maybe you didn't realize, but you're not just... How can I say it? It's also important to kind of like keep in your mind that, especially professors, they're very busy. So like...

I'm sure Ryan, when he, when he shoot the emails, he had like a very precise, like, Hey, um, I need help with this thing. Like I'm working with this other thing. I was reading this paper and like, um, I, I, I do not know how to, how to go from here. And it's very different from just shooting a cold email and being like, Hey, can I do research with you? Like, like you're not, you're probably very likely not going to get answers from that kind of thing. Right. But like, if you're, if you're, um,

honest and serious and have these honest, genuine questions, don't be shy. Worst case scenario, you're just not going to get a reply. But if it's a genuine and worth it kind of thing, you will. I remember there was this one time I was writing a paper and I was in a short deadline. I think like

I was three days away from, from a deadline and I shoot another guy an email because I needed, I needed, I needed to write the related work section session and his, his work was related work. And I needed to compare some particularity about his, his paper and his implementation. I swear to God, it was like 1am and he replied to me 1.10am like, Hey, how, uh,

"When is your deadline? Because I will get into it and if it's very urgent, I'll get it back to you in one day." And I'm like, "Shit. Wow, dude, thank you so much. Why are you even replying emails at this time?" But he knows the struggle. He was genuinely really helping me out. And I don't know, he was also getting a citation. So there was that.

Well, I was not going to say anything because I was just this hobbyist not working on a paper and not really asking for anything except like I clearly, again, clearly read the paper, right? Asking questions that are actually about the material. I think people just get so excited about that, you know? And I totally understand it because again, like unsolicited explanation of CS is not appreciated. But like when people ask me things, it's like,

is like magic so I'm sure I'd be the same it's just hard to like humanize these people when you read their papers you know especially some of the like really like brilliant stuff where you're like I would never have thought of that my entire life right but like these people are just people and they actually like especially the really advanced stuff they love research right almost by definition you know it's a joy right it really is

I usually joke, but there's a hint of truth to it. Like this podcast is mostly, it's an excuse to get, you know, like to hire an incredible person to be here talking and telling me and teaching me things for an hour, two hours, three hours. And by the way, we're recording. Let's share it with everyone. But.

But I absolutely relate to that. I am the one getting the most out of it in some sense. I don't know how these will be published, but I feel like from my experience, I'm following up the Bell Labs guy, which is insane. It's like that's a crazy thing to follow up.

Another example of this kind of thing happening that segues into more stuff I want to talk about is Owen Arden. I reached out to him about his paper. He does security type theory. Most people don't know what that is. So this is like DCC, like some of Abadi's work and blanking on names. But non-interference is the main thing. And it's like keeping people's information from leaking. Really cool stuff.

And again, just hop on a Zoom, so excited to talk, right? Just blab, yap about fun research, right? For like an hour. And he's at UC Santa Cruz. And UC Santa Cruz has language systems data, I think. LSD lab.

Which is very fitting for UC Santa Cruz, I'm just going to say. But I was not a UC Santa Cruz student, but I was with someone who was romantically. And so I ended up spending a lot of time there during my gap year and

They were super nice. They have researchers come, such as Dan Plukin here, come present their work at UCSC remotely. And I ended up going to a lot of those talks just because I've never been a UC Santa Cruz student. I've never been part of their staff or anything either. And you can just go in and watch really good talks by anyone.

great researchers like Dan Fluke in here. And obviously Dan presented and I watched his talk and it was great. And I told him that I was a fan of type theory for all because I am and it was really exciting. Well, it was great. It gave me a lot of credibility because nobody knew and then you said, wow, it's Dan from the podcast. And then everybody closed their laptops and I said, oh, apparently this guy is somebody I should pay attention to.

Maybe that's what everyone should do. We should hire one person. Like, hey, oh my God, I know you're that guy.

like what podcast right but like some other people i was not the only one knew about the podcast and thought it was pretty cool yeah when i first met pedro i i was you know we were just like hiking or something like that and i was like wait i because i you know you don't even realize that like um you know these podcasts are made by actual people and so i was like oh my god wait you make that thing you're

You're just here in front of me. You're just hiking. So that's really cool. Okay. So we talked about, is there more resources we should talk about? Well, I wanted to mention Cody's Church of Logic, which you've already mentioned, but I like it a lot. It's a fun one. He was complaining the other day that it's really hard to edit his stuff. I'm like, dude, you work on fucking AWS. Just pay someone like a hundred bucks and edit that for you. Come on. Just say your stuff, man. Yeah.

You hear that, Cody? If you're listening to this, just come on. Come on. It's not that expensive. His frequency has gone down as well, unfortunately. But he had some really good linear logic stuff lately. And I learned a lot.

Catsters is a category theory YouTube channel that I have to give a lot of thanks to for teaching me what monads are and adjunctions and string diagrams. So that's great. They're a little more advanced. I would start with Bartosz Maluski. And then the last thing, oh, I already mentioned Handmade Network for low-level stuff. So Randy, Ryan, Fleury, Casey Muratori. People are going to laugh that I include Randy, but I am.

And I think that's everything I have on the list. Um, I learned a variety of things from people that came on the type three for all podcasts. Uh, I think I mentioned in the discord that, um,

David Christensen talked about quotation in his episode. I sent him a screenshot of that and then he replied, oh my God, thank you so much for sending me. It just brightened my day. Thank you. Bye. Tell the story. I ended up listening to the David Christensen episode like a few days before my interview, just coincidentally, not like planned or anything, but he talked about quotation and

Yeah, for my current job. Yeah. And...

They were starting to switch. It's a kind of weird thing. I worked at this job and then I left the job and then I came back to the job and I had to interview the second time. Anyway, it's a whole thing. Come on, they already know you. Why do you need that second interview? Just like, come on, make your decision. I didn't standards or something because the most people there are like PhDs and I am not even a degree. So it's a, I get it. They upped their standards while I was gone.

But I passed the interview, and part of passing the interview was they asked about metaprogramming because they were switching to Elixir.

And I was like, oh, yeah, Elixir, totally know it. Did not really know it. Metaprogramming is like the thing that I know the least because when I say I didn't know Elixir, at least at that point, I mostly meant that I knew like Haskell, right? Which is, you know, it doesn't really have the same metaprogramming situation. And...

they wanted me to talk about metaprogramming and I had just listened to the episode on quotation. I was like, ah, quasi-quotation. Yeah, yeah, pretty cool, huh? And they're like, ah, you know about quasi-quotation. Great. And I'm pretty sure that was the most impressive thing I did in the interview, which is hilarious. So I think that was a significant contribution to my life. I think Pedro is entitled to a portion of your income now. LAUGHTER

Yeah, well, if listeners have some similar stories or things like that, please, please send them in our way. I love those. They really help us keep going. You don't need to... That is an incredible support to the show for sure. So I really appreciate that. And I always submit them back to the...

to the person who was interviewed and they're always very happy with it as well. As Ryan was saying, we are all very passionate about these things that we're doing and it's not always that we have the chance to be happy all day about these things and other people being interested. So often enough, I have no idea if anyone is even watching this stuff and then all of a sudden someone shows up.

it really makes a huge difference, right? Like really helps us keep going because, you know, there is costs and time and a lot of logistics associated. Yeah, this is probably a good segue point for me to introduce the notion, for me to advertise that I'll be opening a marketplace. Hopefully by the time that this episode is out, there will be a Type 3 for all marketplace out there. So yeah,

I'll probably have mentioned that either at the beginning of the episode or at the end of the episode. So probably the beginning is a better idea. But anyways--

Final thing, last subject that I think it's worth talking about. I know that Dan usually starts getting really tired after two hours of conversation. Talking to me like I'm a cranky baby. No, you know, we all have different levels of social batteries. And, you know, people are going to blame the shortness of the podcast on me now. Don't do this. Like I approve of Pedro's five hour long episodes.

It's already two hours in. I try to keep things around this time anyways. I think we have covered almost everything. Sorry to throw you under the bus. It's not only about that. I'll be a martyr to it. I'll allow it. It is my fault. Send your hate mail. Send your love mail to Pedro and your hate mail to me. Come on.

You will thank the hate. Do you also thank being canceled? Because I would appreciate that. Is that okay with me? Yeah. I confess to Pedro's crimes. I appreciate it.

In a lot of senses, it kind of is. A lot of the PhD you have to figure out yourself too, but you kind of have this relationship with someone who has already been there to help you out. So how was it for you? Yeah, I mean, you definitely hit the nail on the head in terms of skipping to the conclusion after the introduction is such a big thing. One asterisk that's really annoying is...

uh they'll often use terms that are defined in the technical bits even in the introduction right even if it's not even like a standard term they might just be like we'll define this later right if they say that much right um and my advice then is not to be like if you don't know a word look for it in the technical my advice is

Glaze, glaze right over it. Ignore that part completely. That I think is such a big skill in reading papers, at least in the beginning, is being able to keep reading even if you don't know what they're talking about so that when they start making sense a couple of sentences later, you actually get to that point. You're just like, "Okay, I don't know this. I'm going to skip this. Do I know this part? No. Oh, I know this. Okay, cool." And then you keep going.

And that kind of approach where you just glaze over certain things, they will make sense to you later. Right. Especially when you take in the paper all at once. If you start looking through the technical stuff, looking through the technical stuff is hard, mostly because they want to explain how to like they're making it easy to other people who want to prove the same thing.

Right. So it's all about the approach they took with the proof and problems they run into and how to solve those problems. And it's like, as an implementer, it's not really like relevant. A lot of that stuff.

um sometimes it is relevant because that's like the reason it's true right it's like some key unique thing in there but that's not usually the case i mean people are very motivated like uh the conal elliott episode right people are very motivated by elegance right and things that are just kind of beautiful and timeless and fundamental right and so usually it's not going to be some quirk of the way things are set up right it's just going to be like

very natural. You know, that's, that's really what people want in their research. I say usually, I'm talking about maybe the classic papers that everyone should read. There's also a lot of, I don't want to say junk that comes out every year, but like, you know, it's just papers with less effort put into them. That's like,

more likely to be some little quirk. You know, it's not like super natural and fundamental. That's the thing. Sometimes the research starts getting to a point

And this is something that I think I brought to, you know, other episodes is because, you know, like the fundamental researches are kind of done. And now every new problem that is being solved is this very small little detail of this corner case of this particular instance of that problem over there, you know? So most usually, dude, I don't care about that. That's why I'm saying like, it's not every paper that we should be reading. Like this is kind of like,

Okay, if you're interested in that very particularity and you're doing your research in that way, have at it, you know, and it's important to be published. Like Popo is publishing a lot of incredible stuff every year, but dude, I do not care about most of them because exactly of what I'm saying, you know, like it's very technical corner cases of small functionalities, you know.

And that's the thing, like sometimes not even, and other times, you know, like some papers, they did not put as much effort or like still ongoing research in different directions. But other times it's just, you know, like it's just such a small corner case that it's so extremely technical to tackle that. I will say...

There are some cheap papers, like idea cheap, that are fundamental and nice. And that is the fact that we're still exploring the Curry-Howard isomorphism. So there are still logics that haven't been translated to types, for example. And you can just do that. And that's like a paper.

you'd be the first to do it. But that doesn't mean it's like, it's a sort of like filling out the rest of the idea like you're talking about. But it's nice to read anyway, because it's not so technical, right? It's like the fundamental reason it works is this big isomorphism that's actually quite pretty.

So those papers are still fun for me to read, I would say. I'm surprised you didn't mention Phil Wadler because I think Philip Wadler, he's extremely, extremely good into going into math. Like he's basically the inventor of monads because of that. Like as we know in Haskell, because he just went into this categorical theory and

crazy stuff, understood the concept like, hey, we actually got something really useful here. Let's bring this technicality to programming languages. And I was watching this talk from Simon Payton Jones telling exactly this story, you know. So that's also an incredible, really

it's a superpower, you know, like going into different places and, and, you know, like kind of fishing for different ideas and how to intersect those with our, our interests too. Um, that's, that's incredible. And, and reading, reading, I,

I think he's my favorite author in our field because of that. Like he, he has this way, like what's the name of that? Oh, that banana barbed wires, something paper where he's, he explains the fold. Is that a Phil Wadler paper? I found that paper really hard to be honest. The initial ideas are easy, but the category theory is so hard. I'm thinking of another paper that explains, you know, like there's some, some fold. Isn't there,

a Philip Water paper that explains folds. Probably. I like his linear types change the world. That's a fun one. Classic. Yeah. I think monads were invented, I mean, obviously by category theorists, but I think it was for programming languages and computer science by Kleisli. I could be wrong about that, though.

It does take someone like Phil Wadler to make it mainstream though. Right. That's what Simon Paton Jones was speaking in this talk. Nobody could actually go into the weeds of the details of monads and make it intelligible. And he did it and brought it to the mainstream. So that's incredible. Do you have anything to add on that note about paper reading then?

No. I think you guys have covered it. You can also Google how to read a research paper. There's a few good guides in the computer science area. I guess I would advocate it's okay to not read research papers. It's okay to just like, I don't know. I wouldn't be doing any of this stuff if it wasn't my job.

I really admire you guys, the people who do that, who do this kind of stuff. And I do it as my job because I love it. But if it wasn't my job, I would not have the energy or motivation to do it. And I think I feel like a lot of kind of shame about not reading enough research papers, about not being intrinsically motivated enough. Like I'll work from nine to five and then I'll feel shame that I didn't go read a research paper at 7 p.m. Instead, I wanted to like play my guitar.

It's cool. You can just also live your life. And that's fine too. That's what I would add. Yeah, I hope it doesn't sound too much like that's the only thing I do. I mean, I play guitar as well and other things. I don't actually read papers for that big a chunk of my time. And part of that is because I have a job that does not involve reading papers at all.

Part of that is like a lot of other interests that I'm not, that are just not within scope for the podcast. So I agree. Don't feel shame about that at all. I think I would argue that if reading papers was not your job, I think you would read more.

In this sense, because I think a lot of times being a job kind of like kills the joy a little bit, exactly because you're under pressure, there are deliverables, things depend on it. So it's not as much like just exploring your curiosity as much as your responsibilities too. So it's not as fun. I just put it that way.

making a thing a job kind of like draws the fun out of it a little bit you know i would say um

I want to make space for people. This is something I've been thinking about a lot for people who are like me, who are like not smart. Like we're, we're dumb people, but we like kind of get by with like hard work and, and whatever. And we're not, it's, it's okay to be that it's okay to make your kind of modest contribution at whatever rate you have. And that, you know, I, I'm,

I've only gotten this far by just small incremental little chunks. And then it looks, you know, when I talk as if, as if I know something, but you know, I think it's, it's okay to, you know, when I was listening to, for example, the type theory podcast, I thought all that stuff was so cool. And I was like, and, but I, I didn't do anything with it. I didn't even play around with cock or anything like that. And the, the, you know, that's, it's, it's, it's cool to be that type of guy too, who,

is a bit dumb. I don't know. No offense, guys, but I count you...

Let me be your leader. I'll be your leader. The leader of the... You know, I think, yeah. Man, I relate to that. I think that's why we bond, man. I feel that too. And I feel like it's not even imposter syndrome kind of thing because I feel like I was... Man, I was... Okay, so this is a funny one.

When I was in Paris and I was doing the episode with Mario and so the Lean4Lean guy and then when I was in France with Pierre Marie and then we were all grabbing beer and dude, I swear to God, it was 48 hours of deep type theoretic stuff

I was done. I was like, dude, I just want to talk about an image now. And they were like, yeah, let's talk about how does this thing reduce and what is the career? I'm like,

Like, come on, can we move on now? And that's when I realized, I was like, maybe, you know, like, these people are built different, you know? We have to respect everyone's own individuality, you know, like we, the most important thing, like definitely follow your curiosity. Maybe you just put this podcast on and move on. Like, don't do any research. Like, it's fine. It's fine. It's just, it's okay. It's okay. It's good.

I will also say like feeling very okay being really dumb is like not like really dumb, but feeling really dumb, right? It's very important to

Being able to learn these things in this community. I mean for me getting started, right? I didn't know pretty much anything and I was at the bottom of the wide skill range in the in Reddit and discord and whatever and You can feel that right like reddit is famous for making you really feel aware when that happens, right? and it's true, but like if you

I think to persevere, right, for me, who's not doing it through grad school and is not doing it through work, right, you have to be really okay and happy with that feeling and just know, like, I usually say, you know, I'm not competitive, but I'm ambitious, right? I'm just competing with myself pretty much, right? It's in a vacuum. I don't really care about other people being better than me as long as I'm still moving forward.

That's how I feel. And I will also say I'm a lot less ambitious than I was when I started. And I really understand just kind of taking it easy and realizing that that is okay. And you only got one life and don't spend it all stressed, right? Yeah, that's a huge one, man. It's a big thing. But hey...

Walking towards wrapping up the episode, I have one question that I've been dying to ask Dan because we haven't been talking much for a while. But how's the postdoc doing, man? I wanted to understand a little better. You know, like we talked a little bit about dropping out college, dropping out PhD, but you actually went all the way, man. You're like, you finished the PhD, you're a postdoc now. And like, how is it like growing

How is it on the other side? Yeah, the joke that I was going to make then and I'll make now is that instead of me dropping academia like you guys, it's going to drop me in about a year or two when I fail to find a job.

So like that's for in case for a lot of people, they don't even know what a postdoc is. Postdoc is like a researcher who has a PhD, but it's not they're not a professor. So you're still supervised by some kind of professor and you can do some kind of research. In a lot of ways, it's like a second PhD because you have a brand new supervisor working in hopefully a different research area. And you get to kind of start from scratch, except you actually know how to read a research paper. You actually have some expertise. The postdoc

It's very cool. I wouldn't be doing this type of stuff if it wasn't my job. I wouldn't be able to. And so it's really nice. And I lucked into it also. Like, it's a very privileged thing to be talking about any of that stuff because I only got into one grad school I scraped in. I managed to, you know, get this postdoc by...

Any PhD students who are panicking about stuff? I just sent a Twitter DM to my current supervisor. I was like, hey, this stuff is really interesting. And do you have any remote work for me? And he said, yes.

So, yeah, it's really nice. And in fact, a lot of professors seem to be, even though like a postdoc is a lower status position than a professor, I think a lot of professors are jealous of me because I'm living their dream. I just get to do research all day and I know what I'm doing like they do, whereas they have to like, you know, write grant proposals. I mean, I kind of have to write grant proposals too, but they have to teach and

Like, if you're a professor, the only way that you can really do research is by delegating it to somebody else. And so a postdoc is a really good opportunity to try that type of stuff. Would you say that even, so your professor is actually in Denmark, right? So even there, you think that he has less time to do research than a postdoc?

Because it's a little more balanced than the US, right? Yeah. Well, he's like super senior. When you're a very senior researcher, you definitely don't do any of your own research, I guess. You just have a huge fleet of servers that you just farm off research to.

It's like really it's really like a business. Academia is really like a business where you have to if you're a professor, you have to start having employees and managing them. And you don't you don't I mean, you can find some time to to, you know, write your dream paper or your favorite programming language, but you're kind of doing it on your free time.

It does. If you're doing it like during work hours, it, it, you're, you kind of can tell that you're not using your time very efficiently. You could be using that time to, you know, be writing a grant proposal to get students that would do that work for you. But it's, it's not as fun if you're not doing it yourself. Um, so yeah. What was the question? How is it to be a postdoc? Oh, it's, it's really nice. I think another, another thing is that I got very lucky, like

people who drop out of, uh, various parts of academia or anything. Uh, it, it seems like the main problem is, uh, somebody is, or some system has power over you and you feel helpless in that situation or you're, you're just not having a great time. And I've been very lucky that I've have, uh,

you know, at both of those jobs that I've had so far, nobody's been trying to exert power over me. And, um, a lot of professors they'll, they'll drop out of academia because, you know, then the tenure committee or whatever, or just even reviewers in general, it feels just very unpleasant. And then they go to something else. Then you get a job and then your boss sucks in, in industry. So, you know, the, there's nothing you can, you can kind of do, um, you know, but so, so my life is going well, but I'm,

I'm really, really lucky and I wouldn't say that it's indicative of very much. - I will say working in startups, I think the entrepreneurs starting the companies feel like some of the least free

Because of how they run around getting the attention of investors all the time. And then once they get the investor, now you're on the investor's leash in a way. Absolutely. It's an interesting atmosphere. And I stay comfortably in my engineering chair the whole time. I don't envy that role at all.

But I know that in a lot of kind of even kind of software engineering roles, some startups and companies, they encourage people to like do some kind of like reading papers or some kind of researchy type of thing. Do you know like of the kind of people that you know who work in industry or based on your own experiences, is that the case still?

Yeah, so you get some self-education budget. They paid for a decently expensive Kubernetes course for me.

But that's, you know, it's again kind of based on the things that they want me to know as an employee there. So it's never going to be PL as far as I can tell. Unfortunately, there's no applications to my research because I just do it because it's pretty and aesthetic. I mean, there's a lot of PL research that has applications, but not mine.

I don't care. I think, you know, it's kind of a similar problem. Like, if you're in academia, you can work on whatever you want as long as you can make a case for it in an academic kind of way. I was thinking about, like, if you look at the top 10 programming languages, whatever they are right now, how many of those came out of academia? Like, none. Maybe Haskell, if it's a top 10 programming language. But how many of them... I'd be surprised if it was. But how...

But how many of them use ideas that came out of research? LR parsers garbage collection and stuff then then yeah, so academia selects for a certain kind of Worker which as I guess idea generation and then you have to kind of pitch it in the right way and like 90% of your work in academia is not researching it's trying to convince people that your research that you did was actually useful and

And you present it as if you had a problem and then you solved it when really you just wanted to do something cool. And now you have to tell, you know, you have to find a problem. Yeah. And I have to find a problem. Exactly. So, you know, it's it's it's all hell everywhere. Kind of kind of unavoidable. You get to pick your hell, I guess. Yeah.

Yeah. And to me, that meant, well, I just wanted to say to me, that meant I think the underappreciated route of like work that, you know, you like ideally, but like isn't necessarily your biggest passion. And then, you know, not committing a lot of time to things and then, you know, having the money and space to just kind of relax and do what you actually enjoy. In my case, that does involve reading papers a lot of the time.

Just creating that space outside of your income sources and your places where people would have power over you, et cetera, right? Where it's really just this like, all right, I found some time for me. This is my fun exploration time. Then you can really actually find the joy in it, I think. But one thing that I was thinking is that

One thing that people do a lot with postdocs is to take this opportunity to be more, you know, like have more papers out, you know, because usually we do not have enough time to have a very strong publication CV on our belt to get, you know, like an academic position, a tenure track, whatever. And they will use the postdoc to try to, you know, like,

do first authors or be in many different projects at the same time, work with many different students to get more papers with their names kind of thing. How is that going for you?

I mean, look me up on Google Scholar. I'm not doing a very good job. I mean, that's what you're supposed to do. You're supposed to, you know, that's kind of one of the tricky things about the postdoc is that it feels a little bit more publisher parish because you're supposed to know what you're doing. Whereas before you had an excuse. Yeah, I don't know. You're supposed to do it. Or, you know, or you can think of it this way.

You can think of it as even if you get into grad school, which is, again, like a lot of our listeners, I expect you probably didn't even might not have gotten lucky like like we did to get into grad schools. And to a big extent, it is a matter of luck for sure. You if you are privileged enough to get a Ph.D. position, a postdoc position or a professorship.

and then you're not doing a great job, you can think of it as, well, I have three years to do whatever the hell I want until my contract ends, and then they'll throw me out. But until then, I can just do whatever I want. So I've just been treating – I treat the PhD as like a vacation where I could do whatever I want. I treat the postdoc as a vacation where I can do whatever I want. It would be cool if that continues to work out. Yeah.

I don't know. You've caught me on a day when I feel like I have a Hawaiian shirt on, but most of the time I'm completely panicked about it. I'm not publishing enough. I got it. I'm like, Jesus, I wish I was like that, man. Because most of the time, the mere thought of me being dropped out of the PhD caused me huge anxiety. Like, oh my God, I'm not being productive enough.

But yeah, man, thanks for sharing. Thanks for all the honesty. That was really deep and very vulnerable. I really appreciate that.

With that being said, I think we're good. I think I covered everything that I wanted to cover. Is there anything else you guys would like to bring up before we finish it up? Ryan, what's your latest kind of project that you could draw some attention to? So I'm in the middle of a blog series on Sequin Calculus right now.

in the spirit of helping people read papers, because that notation comes up a lot and it's kind of scary and not well explained. So I have one of those out and I have a linear logic one coming up as a sequel. I have a little VM in C, but it's kind of buggy. But I'm exploring this very different way of compiling functional languages where there's no garbage collector and you do a lot more cloning.

It's kind of like if you did Rust, and then any time the barochecker complains, you just insert a .clone. And this is related to some really cool research by the Gibbon compiler that I would encourage people to look at, because you get a lot more cache locality. Things are located in arrays and things like that. And you can do SIMD optimization. But right now, it's like 600 lines of C, if that. So it doesn't have all the fancy features.

but it's kind of cool. And I got a lot of stuff working. It does have a bug and I'm not sure where it is. That's kind of the state of a lot of my projects, unfortunately. Um, and then I think I mentioned that, uh, Andrew Marmaduke has his Cedil too, that y'all did an episode on. And I believe I have the most complete Cedil to implementation on the planet. So that's kind of cool. Um,

And yeah, that's been pretty exciting to work on. Does the syntax change a lot from Cedil one? I dislike Cedil syntax a lot. So I changed the syntax a lot. But now you do not have all the perks of the... They have some Emacs plugins. I don't have the LSP experience for sure. That comes later. Right now I'm just trying to make sure it even works.

Because that is a very cool experience of SADiL, the whole stuff, like Agnes style, but with different stuff. It's pretty cool. Yep. The developer experience needs work, I can say, as someone who's written a fair amount of Candle code at this point. It sucks. But no, it's really cool to be able to have gotten this far. And Andrew Marmaduke was very, very friendly and helpful.

and patient with my questions. So I've managed to make quite a lot of progress on that, and that's exciting. And then the other thing, the last thing, is the web framework, Arctic, that I mentioned earlier, and working on my blog, making it very performant and pleasant to readers and everything. And I got the demos working again, so you can play with dependent types in a little evaluator on my site. That's fun.

and see the code for how to do that, which is kind of stolen from Stephanie Y. Rick's Py4All. So that's another resource worth mentioning that helped me a lot. Didn't help me with dependent types because I got it at that point. What it really helped me with was understanding bidirectional type checking. This is a thing that needs more resources, and that helped me a lot.

always dreamed that like if I make my work open source enough, someone else is going to start working on it too. That is, that is the dream come true for me. And it happened a little bit for a parser combinator library of mine. Um,

But not as much as I would like. So please don't feel shy from just forking and working on this stuff. It would make me so happy. And I really focus on tiny, readable implementations with this kind of thing in mind. Like, Candle is like a thousand lines of code.

in one file. Well, so if you guys are interested, definitely go to our website, type3forall.com, join our Discord. There'll be a link over there. Don't forget to check Ryan's blog, ryanbrewer.dev. That has some really, really cool, interesting stuff there. There is this particular blog post about all these papers and resources that we talked about. All of those are also going to be in the links in the show, of the show, in the stream of the show.

I have a pretty extensive wiki that's kind of competing with nLab for category theory concepts because nLab is unreadable. It is not extensive like nLab, but it's got a lot of beginner-facing stuff and just kind of explains it like a normal person instead of nLab. So that's on the wiki tab on my site. Oh, here it is. This one. Okay.

Damn, I didn't see this before. That's pretty cool. Thanks. Good stuff. I struggled so much learning category theory and most of it was bad explanations. So this is my contribution to the world. Damn, man. This is absolutely awesome.

Good job. Maybe you should export this to a book, man. This is good stuff. I love it. Someday, once I collect enough. So thanks for watching us. Have a good day, guys. I'm going to finish the recording. And for our YouTube video watchers, that's just a special... I just did a special motion for them. Audio podcast listeners won't know what I did, but...

I hope you guys enjoyed this episode as much as I did. It was very nice to have a community member over like this. It gives me a better sense of purpose of what we're doing. I've kind of been through some kind of rough times after I finished the PhD. I went through all of those European trips and now that I'm saddening again, you know, I am...

kind of thinking a little more what I want to do, where I want to go. And you know, this podcast has given me a lot of kind of purpose, a lot of meaning. I see a lot of value in what we're achieving here. So having someone like Ryan coming over and saying how much he appreciates this and how much value it brought to him means the world to me, really. So

If you guys think something like that, please just send an email. Let me know. I would really appreciate that. It means a lot to me. Even if sometimes I don't have...

much time to answer the emails or something like that. But I always try my best to answer people. I always do. I don't like being ghosted. It's kind of tough on me. So I try my best to answer people. I don't know how long I will be able to keep it up. As we grow, as we gain more success, which is definitely something desirable, as we reach more people, it becomes a little harder to give everyone the attention they deserve.

So if at any point I end up not answering someone or, you know, like it's not, I swear it's not my fault. I swear I tried to keep it up. And I swear that I really, really, really appreciate you guys. If you're able to and you have some extra money lying around, we definitely appreciate even more some monetary donation. Go to our Ko-Fi platform, type2forall.com.

join our Discord or just send this show to a friend that you think would appreciate. Just, you know, like, "Hey, I watched this episode. I watched this thing here." I think you would like it. And word to mouth is definitely the best advertising we get. That's it. That's it. Thanks, Ryan, for coming over. Thanks, Dan. I love you guys. That was really cool. That was really nice. I'm currently looking for sponsors. I'll put it out there. Trilogy of the Universe.

Maybe to reach someone. I would really love to make this podcast full time. I have some stuff that I'm working on towards trying to make that happen. So I have plans to start Twitch streaming soon. I'm opening a marketplace with some friends, you know, making some merchandising. I hope that maybe it would be able to be open right now by the time that this episode would be open, would be out. But unfortunately, that was not possible due to, you know, all kinds of

bureaucracies and coming up with designs but there's something awesome coming on there's it's gonna be awesome i swear you guys are gonna love it really really it's gonna be awesome so i think i'll end this episode on this on this note awesome stuff is on the way love you guys take care and keep up the good work