#41 The Value of PL (and) Education - Satnam Singh
01:41:04 Share

BANG!

Welcome to one more episode of the Type Theory For All podcast. As always, this is your host Pedro Abreu and today we have an amazing guest that it's been a while I wanted to talk to him. We follow each other on Twitter for quite a while and Satnan Singh is the guy who's coming today and he's always seemed to me like he's a very genuine and human person. So I've always been looking forward to invite him and finally we could make it happen. So Satnan is the

He's not only got incredible experience in the industry, he's also been for a while in academia. He has worked on Google, Facebook, Microsoft, Microsoft Research, just to name a few. He's been a lecturer in Glasgow, Birmingham, University of California for a couple of years. And he has worked with a plethora of interesting tools such as Koch, Haskell, Verilog, TensorFlow,

Just to name a few. These days, he works at Grok applying functional programming to design Silicon for machine learning. So I invite you guys to join us in this incredible conversation on his journey in the field of functional programming and hardware in the past 35 years. But before we get into this incredible conversation, we have a few quick messages and we'll be right into that.

Here at Type Theory For All, we have a mission with open access and open education. We abhor the possibility of getting our content locked behind some kind of paywall. So in order to help us to deliver to you the best of type theory, programming languages and formal methods for free, we humbly request your support through Ko-Fi. Simply go to our website,

type theoryforall.com and follow the prompts. A donation of any amount, even $5, will be of great assistance to our cause. Also, don't forget to follow us on Twitter at ttforall and joining our Discord. We're currently organizing a weekly study group to learn Coq through software foundations. So if you think that's something you'd be interested in, go to the website and join Discord today.

This podcast is made possible thanks to our great sponsors Formoland. Formoland is a formal verification company focused on verifying the implementation of programs in the Cockproof Assistant. They have been working in the verification of Rust and OCaml code for the blockchain industry, in particular for Thesos and AlephZero. So if you're looking to ensure an extra layer of correctness to your program, you should look into Formoland's work.

I usually ask my guests how to properly pronounce their name so that I don't get it wrong. So it's Satnam Singh. Even I don't pronounce my name properly. So the way that I pronounce it is Satnam Singh. It's a Sikh Indian name. And I think if you got like a proper Sikh Indian, they would say it.

a little bit differently. But I think for Westerners, Satnam Singh is the easiest. Perfect. So we are here today with Satnam Singh. Thank you so much for being here. And I'm really looking forward to learn so much with you. You said that your name comes from the Sikh. What is that? So I grew up in a Sikh family. I was born in India, in northwest India, an area of India called the Punjab.

and the religion of my parents is Sikhism. And the Sikh religion, it's kind of came from the Punjab, but Sikhs live all over India and live all over the world. So it's not Hinduism, Hindus are the majority in India. It's not Muslims, it's relatively, it's much more recent.

So it's a religious minority in India, but I would say it's well known and punches above its weights. I think that is so fascinating because I personally consider myself quite a religious person, even though I don't quite fit in any religion.

But, you know, a spiritual person and I have this overarching feeling that spirituality can be so important in so many people, especially, you know, when you're growing up and you are passed along the values of your family and religion often enough passes along those ideas.

So would you mind telling us a little more about the background in which you grew up in and does the Sikh values influence you and how are you still a Sikh? And I believe that you also, I've seen in your website that your family immigrated to the UK at some point. Could you tell us this story?

Sure. I have a very complicated, conflicted upbringing. So I was born in India, in the Punjab, which is this state. The Punjab region is actually split across Pakistan and India. So I was born in the Indian part of Punjab. And I was born into like a fairly poor farming family.

And in the 60s, the United Kingdom didn't have enough workers, people to drive the buses, to work at construction sites. And they had a program of trying to convince Indians to come to the UK to do the jobs that there wasn't enough local people to fulfill.

So my father went over to be a construction worker. He couldn't bring us because he didn't have enough money to transport all of us. He didn't actually have enough money to transport really himself. So he worked as a cook on a boat and sailed to the UK and then through village family connections, got to Glasgow and became a construction worker. And then he worked for a while to raise enough money so that later my mother and I could fly over

to join him. So I was one and a half years old when I moved to the UK. My parents had no education. They speak Punjabi. My father's no longer with us, but even in their own language, they couldn't read or write it. So I grew up in Glasgow in Scotland and I grew up speaking Punjabi, which is the only language that my parents spoke.

And when I arrived in school as a five-year-old, the school didn't know what to do with me because unlike the other five-year-olds, I didn't actually speak any English, so they couldn't educate me. So I had two years of remedial education when I was taught English. And eventually I was inserted back into the pit.

to mainstream. I do remember a time my brain flipped from thinking in Punjabi to thinking in English. And I always feel that it's very important. The language that you think in is very profound and it really affects how you think. It's not just, there's not an isomorphic mapping, right? So one mapping to one language, because each language is

optimized for expressing different things, different concepts, and that has a different set of values. So I had a kind of unusual upbringing. And then I had a brother and a sister, so they managed to learn English from me. So they had a smoother ride, I would say, through school. And I wasn't particularly well integrated. I was this brown-faced kid.

in a class of white kids. I was amongst the first wave, one of the early waves of immigrants, especially to Glasgow, right, from India. So I wasn't playing football. I wasn't hanging out in crowds. So I think when people ask, why did you get into technology or why did you go to university? Why did you pursue education as a path?

I would say there was no other choice because I wasn't working in my uncle's garage or my aunt's insurance company or what all the other kind of jobs I could have had through family connections or connections through your church or whatever. Those were options were not really available to me. My father didn't have a restaurant we work in. So going education was the only path that was kind of possible for me.

Why did I end up doing computing? I've been thinking about this a wee bit, how to answer this question, because you posed it in the email that you sent me. And I think there was like three kind of pivotal, pivotal events. When I was, when my parents eventually managed to buy an apartment for us to live in, they couldn't afford to pay the rent.

mortgage for the whole apartment. So they rented a room out to an Iranian student at the University of Glasgow, who stayed with her family for a while. And when he left, I mean, I think I was maybe about 11 or 12 at the time, he gave me as a present a book on mathematics, like an introductory book on mathematics, lots of illustrations and sundials and Pythagoras.

And we had nothing else to do. I just devoured this book. I just read it, read it, read it, read it, tried to understand every single thing. And I find it fascinating how these symbols somehow connected to the world and were a language about the world around me. So I think that was maybe the initial spark

of interest. So in high school, I played chess and I was in the chess team and the chess team was run by a physics teacher. And I did well in physics. So the physics teacher kind of adopted me. And he invited me to the computer club. So I would go along after school hours and there were these computers. I remember, you know, ZX80 computer, ZX80-1, you know, and then a 6502 based BBC microcomputer.

And these computers just seemed like magic to me. You typed stuff in, you typed a few lines of code in BBC Basic, you ran it, and amazing things happened on your screen. And I just couldn't understand what was going on. How were these pixels changing this way in response to these things being typed at the keyboard? And I really wanted to understand

what was happening and I think my career is trying to understand that, trying to get behind the magic of what's actually happening, which way are the electrons going at a transistor junction to make this happen, this kind of end-to-end view. So I think that was another spark that was putting that through my head. Now, my physics teacher, Mr. McClure, to thank for. Then I really wanted my own computer, but I came from a very poor family. There's no way I could afford a computer.

But at that time, the UK government provided support for poor families for them to buy clothes and buy books. And I went to like a state school, like a government school, but it still had a uniform requirement. You have to wear the school's uniform, which is quite expensive. So I convinced, the government would give my parents money to buy a school uniform. So I convinced my parents that instead of buying me a school uniform to get me one for free from the thrift store,

and to use that money to buy a basic version of this BBC microcomputer. And I might have convinced my dad to do that. So I grew up as a teenage hacker on a BBC microcomputer, writing six-five-minute machine code, hacking all the time instead of playing football and chasing girls and all the things I probably should have been doing.

That became my world, right? It became something that I could get into, that I could learn from development. And it kind of went on from there. So I learned on this computer, I had a data sheet. I could see every chip. I had the memory map, the entry addresses to all the instructions. Like, I still know how to write a character, hey, in BBC Magic, right?

in machine code, LDA hash 65 GSR FFEE, right? So you put 65 in the accumulator and you jump to that address, which in the BBC OS is a code that will make an A appear on your screen, regardless of the graphics mode. So I just totally inhaled and absorbed this thing and I built circuit boards and attached them to the IO interfaces. And I went to university to study physics at the University of Glasgow, and I grew up in the University of Glasgow campus.

And as a third subject, my second subject had to be mathematics. And the third subject, I picked computing. I wasn't initially going to be a computer scientist, but because I'd just done so much computing as a teenager all the time, I think I got almost 100% with no effort in my computing class. I did pretty well in my physics class, but it was hard work. And I thought maybe I should follow the path of least resistance and I changed to do a degree in computing instead. And then the government paid for my education. They paid for my fees, paid for my books.

then I went to do a PhD afterwards, which was paid for by the government as well. So I benefited at the time from really, I think, great government support for poor families. And I think, sadly, a lot of that has been eroded since I went. There's still some of that. But I think that's such a wise thing for governments to do, to really try and close the gap between or compensate for the gap between those that have the haves and the

and have not. And I think that was a very successful program. And the BBC, the people, the TV, the government news channel, they had a government program educating the children about technology because they saw that as being important. The BBC very computer made by Acorn at Cambridge. And that led them to the path of ARM and everything that we still know. It created this computer for the BBC that they called the BBC very computer. I think that was a very successful program.

It got people like me into computing and into that career. And we've gone into education and having tech careers, all based on that. I think that's an amazing thing. I think maybe we don't make enough noise about how great a thing that was. So that's kind of like a

a rough view and then at university i i just loved my teachers i love my lectures and i thought they look so cool i want to be like them right uh so i went on to do a phd and then become actually a lecturer at the university of glasgow in the uk or assistant professor in in the us uh i taught and did research and then transitioned to industry so that's kind of my rough kind of trajectory of roughly how i ended ended up here so uh from you know kind of fairly you know

a family where there was no education really, but son of illiterate parents too. My siblings have done the same thing, gone from there to PhDs and careers in tech and government and industry. That is such a beautiful story. And I definitely agree with you having, I really believe that the power of education really erodes the

differences, the social differences in society. Because I also have this pretty uneducated background in my family. I am the second in my whole family to also pursue a PhD, even though I'm not a PhD right now, but I plan to continue my higher education. And I also see a lot of value in having the government support. In Brazil, all of our higher education are paid by the government.

That also creates a little bit of issues sometimes, you know, because students might not pay as much, have as much...

into the game, like as much skin in the game sometimes, and like they don't value as much as if they would be paying. So yeah, I've seen people, my students in the US often enough, they value their education more than here that they're getting for free, you know? So there's also this kind of slim trade-off that I wish wouldn't exist, right? Because free education is just such a powerful thing in a society. But well, I think I'm a...

I'm going a little off track here because this is also a subject that gets me very, very excited. But you mentioned that you became a lecturer in Glasgow and shortly after you've been in and out academia and in and out industry. And it seems to me that your path

is into industry and also into academia somehow. How did you see that? How do you see your relationship with teaching and being a professor and mentoring maybe, but also seems to me that you also have this strong desire to have a more hands-on impact in industry somehow?

I guess, you know, lots of people get asked, well, why have you chosen this path? Or how did you get here? Why did you go from place A to place B to place C? As if there's some kind of grand master plan and you execute the plan. And every decision you make was carefully thought out decision. You've got a spreadsheet and rationale to explain it. Maybe other people have this, but I would say that pretty much all the transitions that I've made in my life, in my career, maybe

be pretty kind of random and arbitrary and kind of honest for a moment. I'm someone that is very interested in practical application of things. And that is one thing which makes me kind of oscillate between academia and research and working in product groups. But I think

I mean, I can maybe sort of just go through some of the transitions and just give some background about why that happened. So as an academic, we had a permanent, I was lucky to get a permanent position as a lecturer at the electrical engineering department at University of Glasgow after my PhD. At one level, it was like a shocking failure because after seven years of education, four from undergraduate and three for my PhD, I had moved literally one block

down the street because I went to high school on the university campus. I went to Hillhead High School on Oakfield Avenue. I eventually became a professor. The electrical engineering department is on the same street, one block down from my school. So other people's education takes them very far, but my education just literally took me one block down the road from my high school. And then I transitioned to the science department. And I love to be a lecturer. I love teaching.

I love explaining ideas and I love questions from students. And maybe other people see it as a cliche, but I really believe teaching is like a bi-directional kind of thing, right? Both parties are learning something about this and it's kind of an interactive kind of thing. And I kind of miss that part.

But I also felt some of what you alluded to earlier on. So in Scotland, undergraduates don't have to pay for education. The state pays to educate if you're a resident student. My daughter actually is at University of Strathclyde in Glasgow at the moment, but she wasn't resident, so she's paying her form fees. But she gets good value for money because people at Conny McBride teach her.

So some students are brilliant. Some are still my friends. I had dinner with one of the students I taught, so the graduate, just two weeks ago for my birthday dinner here. So some of them have remained lifelong friends. Others, they were just following the...

being just washed forward along the path of leaf resistance. And I think they didn't know why they were there. They didn't appreciate, I think, how much the state was spending on the education and how much effort I was putting in their classes and their material and preparing the notes, marking stuff. So that was a little bit of a disillusionment, but it was just one factor of many. And the other thing was,

I think I had a lot of success. I was lucky to publish tons of papers, get lots of research funding, be on program committees, but I worked all the time. Being a junior academic in UK was the hardest job I've ever done. I was just exhausted every night. I worked pretty much every day of the year. I earned very little money and I had a small apartment, not particularly close to university, because I couldn't afford to live near university.

I remember this is one month where I had to borrow money from my bank, the trustee savings bank, so I could give it back to back to pay my mortgage with the trustee savings bank. And I thought, this is miserable. This is, I'm working so hard, but I can't really make ends meet. And my salary as a junior academic, you can be just so miserable.

I wasn't particularly looking to move, but I had lots of industrial collaborations. I have one of those companies called Xilinx that make FPGA chips. I saw a lot of my work was making Haskell-based DSLs to program their chips. I go to Edinburgh to collaborate with them a lot. There was a summer, so this is how random things are. My wife is also in computing science. At the time, she was also working as a postdoc in persistent Java.

Sun Microsystems had a project on that. They had funded her project at Glasgow. So in the summer, she was going to be an intern at Sun Microsystems in the Bay Area. And I thought, oh my God, I've got three months without Susan. This sounds a bit miserable. So I say to my friends at Xilinx, can you wangle me some position at Xilinx for the summer so I can go with Susan to Silicon Valley so we can be together? And they do a bit of research and they make me an intern for the summer. So I arrive as this rather old looking intern. Yeah.

So I can be with Susan. So Susan does the stuff with persistent Java at Sun Microsystems. And I sort of hack and Haskell and generate circuits and make a Photoshop accelerator and FPGA card. And I sort of demo it to the vice presidents when I'm leaving. And I thought, well, I'm done. I'll go back to university.

And on my way out, they said, "Right, that was no bad. Here's a job offer, come and work for us." Which kind of like stunned me and stopped me because I wasn't kind of expecting that. So what do I do now? So I thought about that quite hard. And I realized I really enjoyed this practical activity. I joined like right in Haskell.

generating circuits and then from making something real end to end like i wrote the photoshop plugins in c plus plus i wrote the circuits and haskell and generated beach down place i plugged the card into a machine i i ran the whole thing it had this menu option you know xilinx gaussian blur you clicked it and this like i mentioned earlier this entire end-to-end things happen which

I had programmed from the user interface into what happens at the gates on the FPG or the FPG is to implement Gaussian blur filter on this image. And I found that quite exciting. That for me was kind of missing in my academic position. I always had to

do things which had a certain type and style of novelty above the current frontier of academia to get that paper accepted in ICFP or POPL or whatever and argue that and position it. Whereas I think in industry I felt kind of freer to still do quite innovative things, but I didn't have to jump through these hoops and make these arguments.

appeal to one sense of novelty, even when I think there are other kinds of novelty that are valuable, but not valued by SIGPLAN or whatever, or IEEE, whatever. So then eventually I said, yes, I'm going to do this. And I quit my position, which is very painful because I had postdocs, I had PhD students, teaching commitment, I had government grants. I had to walk away from all of that to then just start as a

software engineer at Xilinx. So that's one of my moves. And as you can see, it wasn't like a carefully thought out thing. I am going to go to Silicon Valley and work for a company and carefully research all the companies and interview all of them and decide which one would work for me. It really was, I was handed a job offer on the way out the door and then I signed it. - Wow, that is actually very inspiring too, because you had to walk away from a lot of stuff that was already set and was already happening, but at the same time you were not

entirely fulfilled or not entirely happy. So you looked for... Yeah. I mean, I love the academic aspect and the research aspect of what I did. I think it's just how much time you have to spend, let's say, writing grants. And that's quite lucky. Lots of my grants were funded. Well, I say two or three. I think I only had like one or two rejections maybe. So I was kind of lucky with my grant writing.

But I think it's just the hours, the amount of time and effort and the low pay that really got me. And maybe if I'd endured, I think when you become more senior in the UK system and become like a full professor, perhaps things might have got better then. But I didn't. I kind of felt a bit broken by the system. And for me, I mean, I went to Silicon Valley. This is like...

This is a pretty high pressure place. But being a software engineer at Xilinx was way, way easier and lower stress than being a junior academic in the UK. Isn't that insane? Like you were in Silicon Valley doing the highest kinds of technology and that's still less work than being an academic. Yeah.

Yeah, I think that's part of it because it's kind of focused because I worked at Xilinx. I did like every day. I did one thing mainly. I worked on these DSLs for hardware design to solve customer problems. I was on program committees and wrote papers and things like that. But I had this one main focus and I could really be technical and hands-on. I think what I've tried to do, I've tried to my career to always avoid being a manager and always stay technical, right? I always try and make sure, these days I always try to make sure that my screen, it should have VS code on it.

If it doesn't have the best code, I'm not particularly happy. If it's got something that looks like PowerPoint or a spreadsheet, then that's not a good moment for me. And it's very hard. I'm 58 years old. I think there's not many engineers who are 58 years old that

that these companies that can stay as individual contributors and just stay relevant technically and hang on track takes a lot of effort. And it's not good for your career because the way you get promoted is to become a manager and then manage and drive and define other people's work.

and draw boxes and arrows. So I wouldn't necessarily recommend it if you want to become very senior and wealthy and have a big house. But there are people that manage to do that. And there's some people that combine both. I think Eric Meyer, to me, is very inspiring. He's someone who's so super technical, but

is also he can hire brilliant people, create fantastic groups, convince VPs about why they should, you know, Facebook or why you should invest. And also publish papers, which blows my mind. Yeah. But I think, but he's kind of like a very rare example. There are people like that, but there's not really, not really many people. For most people, the path

right is into kind of management and running a big running a running group and then you come distant from the from the technology that's always made me kind of nervous because i don't i mean just because i'm you might have some skill with technology program this does that mean you're a good manager does that mean that you're a good leader does that mean you can do the corporate politics or the university politics or the politics of government to get this center funded or whatever or evaluate these people so i think that's

I think a strange thing in our society that you get your training in one particular thing, and then you're asked to do other quite high level, very critical, important tasks for which you have no training in background. And the fact that you are good at programming is not a proxy of you being good at these other things.

And that also translates as being a professor too, because it seems to me that most of the actual professor work is not entirely related to their technical knowledge at all. It's writing, it's mentoring, it's lecturing, which we don't have formal training during college or higher education either. Absolutely. I felt completely unprepared to be a lecturer, to be an actor. I made a lot of mistakes and I had to learn a lot on the job.

I think in education we focus too much on the formal courses, right? Right. Your course in calculus, your course in programming. And every so often I give lectures about what does it take to be successful in industry or successful to be working in a research lab. I always try to emphasize to students the importance of developing other skills like communication.

communication skills, right? You have learned how to read, learn how to write, learn how to persuade, learn how to analyze information, distill it, work out what's important, what's not too important, learn how to forge relationships with other people, learn how to convince people to win over your ideas, et cetera. Because when I look at my peers, like who are the people,

people who are actually successful in the companies I worked at whose names begin with VP and things like that. They may have been programmers early on in their career, but they've got to their positions of influence per...

Unless your name is Eric Meyer, you've done that by being good at communication, by building up a network of people you know who you get some respect from and being able to persuade people to go one direction rather than another. Be able to explain your ideas and convince people about your ideas, especially non-technical people who have got to make the funding go no because these people

will make their decision, not based on understanding the technical ideas. They can't. They're going to make it by trusting you. It's their trust in you that's a proxy for whether this is a good technical decision or not. And the further you go along your career, the more and more of these aspects of communication, your network, the people that you know that you've built up with,

become like just critically important for getting important things done in the world to do with teaching, to do with technology, and to, you know, improving world. It's not just coding. It's not just, it's not just this and that. But somehow I don't think enough of that is taught, right? Yeah, exactly. And it blows my mind. I always see my peers working so hard. They're so smart, so intelligent. And, you know, like they could, they could

crash me any day on any coding interview because they're just thinking a different frequency than I do, right? But I see so much more value often enough in the power of communication, of networking. And I try to show that to my peers sometimes, but apparently people are often so

caught in the game and like looking so straight, narrow in front of them that they have to work so hard in their hard skills that they completely forget about their soft skills. And I think that's a complete shame as well. But, you know, you're saying all of this and I'm still thinking of this decision that you've made about dropping academia and going to the Bay Area. Could your wife join you back then? No. Did she also get it? No.

No, she had to finish her PhD. So we lived two years apart. That was a big test of our relationship because she had to finish her PhD. So we had two very difficult years apart. And then at the end of that, she wasn't my wife at that point, she was my girlfriend. And after that, what Susan said was, well, if we can survive two years apart. You can survive anything, yeah. I think we can.

and get married. And by then we'd be together for 10 years. So when she finished her PhD and moved over in 2020, we got married, you know, we moved together, moved to her son's house. And then May 2020, we got married. But yeah, that was a very difficult thing. And I know many people who have this kind of two body problem where they're forced to, for certain periods of time, live apart. It's a notorious problem in academia. That is very nice. And I'm happy for the both of you. Congratulations.

You've made it. Thank you very much. So moving forward, before that, you know, like another another thing that has been in my head is so I'm from Brazil and I've pursued higher education in the US. And once I reached there, I ended up, you know, like I was doing my Ph.D. and now and I ended up dropping the Ph.D. to just get a master's. And to be completely honest, you were talking about, you know, like how hard it was to be a lecturer and I

I want to talk a little bit more about that, if you don't mind, because, you know, one thing that I've noticed in the U.S. is how much the higher, to be entirely honest, to be completely frank with you, I feel that the higher education system, especially in the U.S., I still want to learn more. And maybe you have some insights about that on how it is in Europe in general, maybe the U.K. in particular. But in the U.S., the higher education is just such a money grabbing system, you know, like it's

it makes me feel, you've also been a lecturer in some institutions in the US, so I think you might see what I'm getting at. But I feel that education itself in the US is not the point anymore. You know, I feel that all the time they're just trying to

make money, to grab money from the students. And you can see that even in their interactions with junior faculty, it's a common theme. You hear, like, senior faculty is telling them to not worry so much about teaching, that leave that, put the least amount of effort into that because that's not what's going to count for tenure sort of thing. And that's just one of the many problems that I see, you know, like the point that I'm getting at is it feels that education itself is not the value. And that makes me pretty

Do you ever feel that? Do you see that? Is there any difference between the UK or Europe between and US? What are your thoughts? So, yeah, there are lots of differences. But let me perhaps turn your questioner's head a little bit, because you've kind of asked how are things feeling in the US and how could we feel? And I agree with every single thing you've said. I've actually never held like a permanent position as an academic in the US.

I've been an adjunct at the University of Washington, when I was at Microsoft, I taught a course of chip design. I recently taught a class on hardware design at UC Santa Cruz just as a temporary lecturer. But yeah, I've not held any proper academic position in the US, nor do I want to for the kind of reasons that you...

Rather than thinking what's wrong and all the things that are miserable and all these people who are spending all the time writing grants and having these big giant groups of PhD students, I would say to you, look at some people who are doing, who are great role models, who are doing great science in the US. Look at Nate Foster at

Cornell. I think he is a fabulous academic. I think he does excellent research that is really principled of the highest quality. And he has a very successful career. So it's the existence proof of can you actually work as a scientist that is really driven by principles and value, as well as want to nurture talent and give back to community. He seems like a great

He sees that as a great example. Anyway, I could probably think of a lot. Let's look at Stephanie Vyrich at University of Pennsylvania. Amazing scientist, does wonderful work, a great mentorship, developing the community, educational outreach, absolutely inspiring figure. She's a professor in the

in the US system. Look at Adam Chappelle at MIT, who does this amazing work that tries to map some of the most hardcore theory with some of the hardest practical problems in the world. I don't think he's some kind of money grabbing fiend. He's a person of the highest principles and values. And I think he's an inspiring figure and has a great career. And there's so many names, I could just spend the whole podcast just

talking with people. So rather than looking at some of the professors that we might both be thinking about, where he talks about building up a big empire of students and postdocs getting tons of money from NSF and so on and cranking the handle and getting new students and plugging them in and cranking the handle and injecting them out. Of course that happens. And in some degree that happens in the UK and Europe as well. Forget about that. If you're

want to work in this field, in the field of programming languages and theory and so on, and do good stuff. I think there's definitely possible, there are chances and opportunities there. And you just look at the existence proofs, look at the examples of the people that I've seen, all who I think are aspiring, wonderful people that are doing great things. I love that answer and gives me, definitely gives me hope and helps me to look things into a better perspective, into a more hopeful perspective to move things forward.

Shall we change the topics now a little bit and get technical and talk a little more on, you know, your what seems to be the overarching theme of your career, which is formal verification of hardware? Where should we even start? Well, I mean, I would say that I'm not sure that's the main or even the key thing. No? Well, so...

I'm on LinkedIn and every day I get people asking me to go and work or interview for some company. So what do you think might be the number one thing I'm asked to write? I mean, at the moment there's a lot of critique in machine learning, but that's kind of a relatively recent thing.

let's put that to the side, right? It's pretty much the majority of people that want me to interview. They want me to interview to be the head of DevOps at Citibank or something like that because the most successful thing I've done in my career isn't

a total representative of my career. Because I was lucky enough to be one of the early developers of Kubernetes at Google. I think I was one of the top committers in the early phase of Kubernetes. And that project has gone on to be hugely successful, runs the internet. And as a consequence of that, that's, I mean, outside your research and academia, the people who want to hire me or look at my research profile, that's what they see, right? That's the kind of thing that they kind of know me for.

So that's another kind of randomness in your career. Like, like everything in life is just so many random kind of things. That's the one random turn I took where I worked on something which is nothing to do with my background. And it turned out to be the most successful thing I've ever done. I'm disconnected from all the other things that I've ever, that I've ever done.

So the formal verification stuff is largely inspired by my PhD advisor, Mary Shearer. So I did my PhD with her at the University of Glasgow. I was her first PhD student. The second was Graham Hutton, my academic brother. And she's now a professor at Chalmers Technical University and has had many other great students crew in class there, for example.

So, and I think she's always been, of course, interested in problem verification. So I caught some of her interest in this as well. And when we worked together on this kind of lava system, it provided us workbench to try ideas. Now, one of the best examples of that was a project that we did with Guna Stolman. This is when I worked at Xilinx.

She was at Chalmers, you know, goodness, Lomark had his own company, maybe he still has his own company. And there were some ideas about, you know, key induction and SAT solvers and so on. And that idea was not mine. Yeah, that was, I think it came from me to Grubb. I did some of the hacking and implementation and we were able to build this pre-collected end-to-end system where at

We could design some circuits, improve these properties as bound in ModoCete and create useful circuits that run in FTGAs that have these Bob approved properties. So we all like combine our each person brings a complimentary skill, you bring it together. And that was our sheer and storm arc saying 2000 people. And I think that's my most cited paper. That was electrifyingly exciting. So that's what that

That's the kind of things which I like doing, right, with formal verification. It's just finding ways to actually build an actual system which implements formal verification ideas and runs them end-to-end. I think part of this is inspired by a view to... I wish computing was a science or engineering discipline. And I...

I feel, I personally feel mostly it is not, it is a craft. And I look jealously at people that build bridges or remember when I was doing physics about having all these models and laws of the world and you could calculate and predict

and create professional bodies and processes and how things are done and guarantees and then be able to get insurance and legal statements for what can and can't happen, et cetera. And I think software, we're just so far away from that. But I think we need to get more in that direction. And so my interest in mathematical formal aspects of computing are all about can we drive more computing into that part of the space where it feels more like science or engineering rather than

a craft because you know, and there's this project, you know, we did a, I mean, it's by, you know, by work with people like Adam Chapala, there's a project that we did at Google called Silver Oak where we try and bring together specification, implementation, and verification. I dislike that these are three different activities done at three different phases done by three different groups of people. I just want this to be the same thing.

There should be no difference between these things. And Silver Oak was an experiment where we tried to make a silicon root of trust system, which is like a mixture of hardware and software, which tries as an experiment to push that kind of idea where we, in the Coq theorem prover, wrote a formal spec in Coq of what this AES hardware should do, what the software, the driver software, how it communicates with a little bit about the bus that communicates between the two. Then we made a DSL in Coq

that which describes the hardware down to the gate level, which we can extract the system of our log hardware. We had a DSL based on work done at MIT that describes the software for which we can then extract RISC-V code. And we were able to then prove that this system matched the spec

that we wrote in Cockaberry, all in one system. And it was all, it was one, there was no formal delineation, right? I mean, it's all one thing, it's all a bunch of cocks, some was a spec, some was implementation, some was proof. And we just pressed buttons to automatically get the code out of that. We should then place the root, put on our board,

and run and the whole thing does the right thing. That to me feels now like engineering. That to me now feels like science because you now have some kind of formal account of what this thing does. You still have this trusted computing base, it's your formal specification, but everything else is then built on top of that and you can relate which way the electrons go to transistor junction to what you wrote in your Coq spec. I think that's a great thing and I think we need to have more and more of that

in the world, but it makes us, I think it means that I think all engineers should value and understand the importance of specification and clear specification and implementation and relating implementation to the specification. So I find that electrifying and exciting. It's hugely hard. I mean, I did this project myself, had a wonderful team of people that worked with me for doing it. This is still kind of,

of PLDI paper kind of stuff. But I think the industry needs to make this more and more mainstream. So my interest in hardware kind of stems, my interest in hardware verification is like a part of that. The hardware verification I do at the moment isn't like that because at my company, we design the chips and system by a log, not my...

using my Lava DSL. So we write SysAverlo, which is this incredibly amazing language that has got wonderful features in it, including something that pretty much looks like LTL logic, disguised as a regular normal hard description language. Engineers write without realizing that it's LTL logic.

And then the companies like Cadence and so on make model checkers, which can then try and formally prove the properties that you're specifying, which I think includes the SSS algorithm right from 2000. So that also I think is amazing as well. And I think the hardware world has kind of led that a little bit with this use of writing formal properties and then getting a tool to check them.

And we're beginning to see more and more of that in software, right? You've still got in Framacy, you've got this wonderful tool where you can write post-preconditions and do horological style proofs. We've got Daphne, which I think is a great tool where you can try and write

process wonderful IDE and great support automation. Even in Haskell world, I think you've got really inspiring things like refinement types with the work of Ranjit Jala and their group. So we've got little bits of that in the software world, but it'd be great to have much more of that. It'd be great to repeat some of the success we've seen in the hardware world, checking certain types of formal properties

automatically having that become pretty much a standard part of the silicon chip design flow. - So you mentioned that you have a, that you're working on Grok with all these silicon chips. Can you tell us more what you're doing there? - So Grok makes chips to accelerate machine learning algorithms. And you can view our chips as being like linear algebra accelerators. So they don't look like processors. They try and do matrix multiply very, very quickly, 'cause that's the key heavy duty computation in machine learning workloads. So if you look at our chips,

If you look at a floor plan, the version one chip, they'll have these huge big engines called MMX, matrix multiply engines. And then there's lots of distributed memory, there's kind of vector processes, waste compute value. So you have this kind of spatial 2D, 3D compute engine where data is moving kind of in lockstep, getting multiplied, added, relude, restored memory, read from memory, permuted. And you can get...

all these transistors firing at the same time doing useful work in flight at the same time, you've got a phenomenal amount of parallelism and you achieve phenomenal performance for especially machine inference algorithms compared to what you could do in a processor. We've built very, very, very performant system for running large scale machine learning models. So we've got racks of computers.

You can try them out, go to grok.com, you'll get a prompt, you can type in a query, you can pick which inference engine, which machine learning model you use, hit go, and you get an answer very fast. Hundreds of tokens per second, thousand tokens per second. That is just way faster than anybody else's solution.

to AI or Google or open AI or Google, whatever. So these chips go, there's low latency, high throughput implementation of machine learning algorithms. So that's a key thing that we're doing. And we're making these specialized chips for doing that. So I work on a bunch of things at companies. So one thing I've worked is in the second generation, the V2 of this chip. So I did some of the hardware design for that, working on some of the verification for that. And I've done some of the compiler work, which tries to take,

these machine learning models and map them into a compiler. And I've written like a domain specific language for programming, I call it HAST, it's like a Haskell DSL where you can write these linear algebra operations and then it produces the IR that goes into the compiler. So that's the kind of things I tend to get up to.

I'm fortunate to be able to work both in the hardware part of the company and the software part of the company. And then I'm also fortunate to be allowed to go rogue and go to the odd conference and hang out and listen to talk. So I'm looking forward to going to PLDI in Copenhagen in a few weeks. What are the kinds of clients you guys have? I'm not sure if I can say that, but, you know,

I think you should stay tuned for that. For right now, anyone can use our models. You can go to our page, you can type in queries, you can ask for API access, you could build your software stack on top of our foundation models that we run. Well, we run other people's foundation models. So on top of our stack, you could create your business on top of that. So we're just wrapping up to the point where we'll start billing

and have a customer side giving us, at the moment we're not charging, but people can build stuff on top of stuff. So we're at this crucial moment. So right now I can't say that, but I'm very excited about, I think our potential. - That is awesome. So through what you were saying about,

hardware and specification and from verification, you really highlighted the importance of specification. I would like to pause on there for a little second and let's take a little deeper look on what is exactly the specification and how it relates to the implementation. And why do you think it is so crucial to have, you know, like think about specification of your software, of your hardware and software? Well, what is, if you want to be an engineer, right, you want to have

If you make something, you should have a model of that. So you could test that if the thing you made matches the model. Just like if you're building a bridge, you have the laws of physics, right? Which tell you how materials and whatever and gravity behave. So you can then make predictions and test it out and make sure the thing is what you think it is. And that's what we don't have in general software. We just have testing. So we poke the thing here and there and there and go, guess, well, maybe it is what I think it is.

There are many reasons you want a specification. Another is writing the specification part of how you think is part of your thinking and creativity process. I think many of the bugs, when you do this approach of writing a spec, making implementation, trying to relate the spectrum implementation, you do it in the iterative parameter. Where are the bugs? Well, a lot of the bugs are in the specification because you got your thinking wrong. So the specifications can be subjected to automated analysis and reasoning.

they just let you think, they improve your thinking, they clarify and sharpen your thinking. And that early on then helps you to avoid problems, which would later on would be debugging problems and test cases that you had to sort out, which you just, that just never happens because you fix that problem at spec. For complex systems,

A lot of the problems are the interface and composition of systems. Someone designs widget A and they think they've done it completely correctly. Someone designs widget B, they think they've done it correctly. In our case, A is a compiler and B is our chip. You put them together and they don't work.

because you know what? AB did not have the same understanding of what was meant to be built because there was some error and some specification or some ambiguity or some non-determinism that was not kind of expected. If you have one overarching spec that both sides can agree to, that makes it clearer to then compose the components and know when things happen.

have gone wrong because it's the integration and composition of these complex systems that are really soul destroying. Those are the types of debugging that takes the longest, right? Some kind of surgical thing in the heart or something, oh, this floating point multiplier thing, oh, it's one cycle too late. Right, I know how to fix this. I move this register from here to there. These two giant complex machines, I put them together and nothing good is happening.

What do we do next? We thought everything was right and it isn't. Those are great examples. Would you say that doing the specification correctly is the hardest part of the job? If not, what is? Yeah, I mean, I

I'm not sure if I want to say that, but I would say trying to specify what you want to do, whether it's formally or in English language text or whatever, is a very, very hard and important task. And I think it's one that we don't often do to the rigor that we ought to, whether it's text or diagrams. And then it becomes a source of problems later on, because I think we don't value it.

the same way as we value code, megabytes, milliseconds, how many minutes is a CI job taking? Can we take it? Can we make it smaller? Because in a sense, we don't cut apply these metrics and rulers to respect because I think one thing to worry about is there's kind of the dumbing down of software processes where you only value things you can measure. So you have this quantitative view and you don't value qualitative things.

because you can't put a ruler to them. And I think that's been a general trend I've seen in industry. I've seen that trend at Google and other kind of companies. And I kind of dislike that because I think we should value qualitative judgments and concepts and things, at least as much as quantitative things. I think sometimes people do this sort of laziness, right? You're a manager or whatever,

And you've got to make a decision about was this good or bad? Do you promote person A or B? Do you use solution P or Q? So you could think hard about the technical nature of something and its pros and cons and its caching structure, whatever, understand its technical nature and then come to judgment whether it was good or not. Or think about this thing this person has made in terms of its structure and architecture. Will it endure or be evolvable or whatever? Or you could look at...

milliseconds, megabytes, tail latency, whatever, and just have a graph. And then you try and drive some numbers down and some numbers up. And then you can get 17 numbers from different things and perform some undefined addition operation with them to come up with some other number for which you make some arbitrary decision, right? And I think we've ended up doing, in our community, we've ended up doing too much of lateral, doing these undefined additions and bogus judgments from the

the sum because it's so hard to do the thinking about the qualities of things because it hurts your brain because you have to think. But things are important and it's important to be a professional and it's important to do the right thing. And sometimes your brain should just hurt you and you have to make that kind of subjective qualitative judgment. True. One thing that comes to mind when you're talking about all of this is I feel sometimes people put a lot of weight into

this idea of being fair, you know, like so an argument for using so much numbers and so much graphs and, you know, like, oh, because this gives us an objective view of and it can be actually fair. And that's

That always makes me feel a little, you know, there's doesn't quite capture what we're trying to accomplish there. Because, you know, when we're doing these kinds of decisions, sure, it's very important to be fair and all of that. But you also have to trust the human ability to do it.

assess the qualitative part of the work, you know, like to look at a piece of software and you don't, you know, like it's good to have the numbers and it's important to look at the graphs and to look at the objective, what is the output that is going on here, but also to be able to trust that a manager here that is in that position for so many years is going to be able to look deeper and

assess it in a higher quality of, well, you know, you don't have data for the amount of actually good things this is going to make and how much value it's going to bring for the team and for the company. Would you agree with that? Yeah, just let me clarify that a little bit about this.

I definitely think you should have graphs and charts and numbers, right? And I think they're important for incrementally improving some system A, right? You absolutely need to have instrumentation in order to improve quality and be able to judge the impact of decision A versus B, et cetera, et cetera. That's just professional software engineering. I think there's absolutely no doubt about that.

I think where I feel uncomfortable is when you've got two totally different systems A and B, and you've got to pick one over the other, or you've got to shut one project down or whatever. If you only look at numbers to decide what to do, that I think is, that's where I worry. Because I think there's lots of things about the characteristics of the architecture of these systems, which are not in graphs and charts form, which might say that, okay, maybe this system is two milliseconds slower than that system today, but...

because of the things coming down the line and the changes in this pipeline and a pivot to this other kind of market, actually this other architecture feature will come into play, which is not delivering now, but it will in the future. And that requires thinking. That requires thought, right, about technical structures. And likewise, you're evaluating people as well, just putting things into numbers and saying person A deserves to get promoted more than person B because person A got 4.7 and person B got 4.5, right? That's where I...

That's why I kind of really get down. Of course, I'm absolutely for metrics and measurements. That's just standard practice. What I don't like is the abuse of metrics and measurements. Then when it comes to academic things, I think I'm a failure of a computer scientist because...

I don't write these papers. I don't write these papers. I don't write graphs and charts papers. I have zero PLDI papers. I'm going to go PLDI, I feel like a total charlatan. Because I'm not interested in making a cash that's 2% better than the cash from last year. But also, I think the problem with the metrics is that the community gets to define

or the steering committee that I'm not a member of and I'm not an in-crowd because I've got no way to kind of define what the valuable metrics are. And then you can just totally game the system. - Exactly. - You see, it's fair. I disagree with you. I think it's unfair because once you define the assault course, you've defined, given the value judgment to what's valuable and what they would give it. And then anyone can game it, right? And then people are doing science for the metrics. And I just find that it's just so, so destroying.

I don't want to be driven by having my creativity ideas and thoughts be driven or even guided at all by the metrics. Companies should do that, right? Companies that know that the next product they're going to launch in six months or whatever. Sure, right. If you work at academia, you're not working at a company. Your job is to do the crazy stuff that companies are not going to think of, that no VP would sign off on or whatever.

and explore, I think, wider, crazier, wilder ideas that would fail all the current metric tests that are in place. Oh, I love that. I love that. And you're absolutely right. That is science. That is science that you're going to say. I was going to say something unwise, but I've decided to, I shall... We can cut it out later if you want. No, no, no. I mean, I'm exaggerating to make

I feel kind of, I mean, I love, you know, computer hardware, you know, like I said, my Twitter handle is satnam6502 after the 6502 processor, but I never ever got into the mainstream architecture community, right? I'm not part of ASPLOS and all these other conferences because so much of that is just graphs and charts and like minor improvements to some cache or whatever. I mean, recently there's been excitement in architecture because of machine learning and new architects, machine learning, chips like my company makes, but

I think for so long, it's just, I think I found it a bit of a dispiriting kind of field. It's hard to like crazy ideas. I used to be very active in the FPGA community. I went to all the FPGA conferences. I published in all of them. I was pretty much all of them. But

And quite a few of my papers published, but most of my papers got rejected because they didn't have the graphs and charts. They were about, here's the DSL for doing hardware. Here's the way of describing hardware, which lets you, the more agile way to describe state space. Here's the way of doing a hardware design, which is much easier to formally verify. So you've got these high level machines. That wasn't valued because there were no graphs and charts, right?

eventually I reach that community. I don't go to any FPGA conferences. I'm not on the committees of them anymore because that community just was, their mind was closed to, I think, crazier ideas that were even slightly off the main beaten path of here's another accelerator. This is how many milliseconds it takes and this is how many megabytes it uses. And this is why it's better than this other person's.

accelerated by 0.2%. That's the only kind of game I think that community wanted to play. So I kind of rage quit. I mean, I also partly quit just through, also due to having a bad manager

experience, which really I found very, very dispiriting. I used to think that human resources had my back and was on my side because that's what human resources does. "Oh, well, tell us your problems. We are here to help you. We feel your pain and we're here to support you." Well, that's not true at every company. And what I learned the very hard way is actually human resources is there to protect the company from the employees.

that's their job. And so in this situation where I had this conflict with this manager, who was basically a bully, a really terrible person. And I went to HR, you know what? He's a very senior person and I'm not. And the company basically made a bunch of decisions that were in his favor and not mine. And that's why, that's what I stupidly, I should have known this, but I didn't. I just supposed to follow HR would see what had gone wrong and try and fix it somehow. But no, the company will,

protect itself. And I was the naive person for not realizing that. So now I know what HR is about. And if it serves a very important function, and these are all very good and important people, but I know they're not there to protect me. This is a great opportunity for us to talk a little bit about bullying in this

the workspace, because I've noticed in your blog that this is something that quite, it seems to me that you've learned a few things and you have some thoughts and some advices on how to deal with people who are trying really hard to shut you off and keep you

away or maybe even have just some personal vendetta against you. Because, well, it would be great if we lived in this perfect world where everyone could deal along very well. But that's not the nature of reality that we live in. And sometimes, you know, personal ego, personal problems. And sometimes people just decide to try to wreck your career or whatever.

all together. Could you share with us a little bit of your experiences and what you've learned? So whenever humans get together, there are ways that wonderful things happen and terrible things happen. And there's all kinds of characteristics of human-human interaction that occur from whenever you've got two or one or more people together. And it happens in all aspects. It's not just companies, right? It's families, it's friends, it's

It could be your church or whatever. So there will always be people who will be insecure. Insecurity is the root of lots of bad behavior, and that insecurity will cause bad behavior that's inflicted on other people. And that will always happen in companies, and it will always happen in other aspects of human nature.

In a company, it's kind of very problematic because if it's your friend or whatever, or ex-friend, you can walk away. And then you've lost something. You've lost some investment relationship or whatever. In a company,

you can lose your position, you can lose your job, you can lose the passion you have for a project that you're working on. So it's kind of very serious. I think it's very depressing. When the bullying comes from someone who has a position of power over you, that's very, very tough. In general, that never goes well

for the person that's being bullied. Because your options are very kind of limited, right? You could reason with the bullier. I don't think that's going to typically work. You could complain to the company. I mean, some companies I'm sure are much better than others, but in many companies I've experienced,

And I worked at that. Well, they'll separate you. So you invest in this project. You've got this team of people you've worked with. You've built up these relationships. And that all gets reset. And now you have to go to a new project with new people. And then your performance review is going to get dinged because you didn't manage to complete the goals for that original thing. And then some people bark you as a troublemaker because they'll think that you're the person that is going to get all of them. So it's just a terrible...

I'd like to see that there's some solution to this, but it is often just a terrible,

It's just a terrible, unfortunate thing. And I would say, look for early warning signs. If you can see if someone's behavior is heading in that direction towards you, jump or move away, run away sooner rather than later. So I've had a few experiences. I mean, not too many. I would say it would be very lucky. I've actually loved almost all the people I've worked with. I've loved almost all the managers. I love my current manager, Jim Miller at Grok. It was like...

a wonderfully excellent human being and fantastic manager. But I think because I thought when I went through the bullying, I felt kind of alone and isolated. I thought, I'm the only person that this is happening to, right? Everyone else seems so happy and everything else seems so cool.

So I, because I have a bit of a voice on Twitter in a small way in the PL community, I thought, I'm just going to write about this because I can't be the only person, right? There must be other people that experience this as well. So I wrote my article on abuse and just so many people contacted me. It was like a floodgate of people. I mean, I suspected there might be people who had some experience that they just didn't talk about. I just didn't know about them. But I was taken aback by just...

how many? And I'm like, pretty much on a regular basis, every week or every other week, I'm chatting to someone about some situation they're in. I just listen and I have nothing good to say or sometimes I might have some advice or whatever. And it's just kind of ongoing. It's happening all the time, kind of everywhere, but you don't see it, right? Because it's a very difficult thing for people to, it's a very difficult thing

for people to talk about. You see people change jobs, you see people change positions, people are working on this project, they're not working on that project anymore. It seems a bit odd, you're not sure entirely why. Well, often there's a kind of a tragic reason that's kind of behind that. In the companies I worked in, there are certain types of behaviour that are just absolutely unacceptable, you get fired, right? In the United States, we have these

protected characteristics, right? If you make a racist comment about someone, you're out, right? If you discriminate against someone for being pregnant, you are out. I mean, that's quite ruthless and it's very systematically enforced. But then we fall off a cliff, right? There's a whole bunch of other behaviours, there's a bullying that you could do

that's kind of fine. You could get, you'll probably get away with it. The company isn't going to devote too many resources to try and do that. I don't want to speak for all companies, but I'll say that some companies I work for, really, I don't think have done it.

I've not really dealt with these accusations very well. I'm sure that other companies that deal with it very well. I have not worked at all companies in the world, so I can't represent all these companies. So I wish there were aspects of bullying that were all, if we could find some traits and characteristics of bullying and also make them have the same kind of status as these protective characteristics

Then I think it gets formalized, right? Then it becomes the job of HR to act on these things, right? Because it's a part of policy. It's written in paper, written in a document in your performance and whether you've done your job or not. It depends on whether you've taken action against those items. And also building some kind of support system layer where

where the people that is not in the position of power, they feel safe enough to reach out and look for help. Because I remember one time I was an intern somewhere and I felt absolutely stupid in the presence of this other person because he would get just mad and be very angry and say things that could make me completely shut down. And nowadays I can look back and recognize this as a kind of bullying, but sometimes you're

You just don't even know that. You don't even know that you can reach out and that you can look for help and that, you know, like that there are ways to hold conversations and to hold your ground, to try to fix that and make your life better. So...

Maybe we still have a lot to learn and a lot for companies to grow in that regard. Definitely. And it's just a shame, right, that this kind of exists and we're still working on it. But, well, we have hope. And that's why I've been, I asked you this question specifically because I think we have to talk about these issues. We have to make these things known and we have to discuss this to bring them forward and to draw attention to these kind of issues that we may face in our... Yeah, absolutely.

But I think until things get legislated and formalized, I'm not sure what will really happen. Because if you look at bullying in academia, which is a very big problem, especially in life sciences and labs, and so professors have got labs, chemists and so on. There's just so many stories you can read that are well documented, that are in the newspapers. And the power dynamics is just so much more skewed that just makes things so much worse. We've seen this and we've known this for decades.

What is changing, right? We're still... Yeah, true. Nothing. Tomorrow, there'll be another example of a professor abusing their position and their lab technicians or their PhD students because the dynamics are in favor of the person that has these big research grants and run these big groups that get their papers. Unless there's some formalized counterweight to that...

I don't see why things are going to change, right? That's the depressing nature of it. And it's nice to have a support group. Sometimes some people get value of discussing what they've been through with others. Others want to go for it and deal with it themselves or deal with it like I did. I went through therapy to deal with it. But that's just dealing with the wounds. That does nothing to fix the source of the problem.

Well, when I, when I mentioned, just to clarify, when I mentioned support system, you know, like I mentioned, have a system inside the, the HR such that the people would feel safe to reach out and that they know that something would, would go forward from there. But yeah, I definitely agree with you. Um,

Moving forward one more time with our subjects, there's still the topic of functional programming, particularly in the notion inside of hardware verification. And it seems to me that you've done quite some thought. And I think my main question is, what is the value of

functional programming here? So I think for me, so first I'll just speak for myself. I think one thing I've learned the hardware over many decades is I can't convince most hardware engineers to do function where I've tried, but that's not what they want to do. System Verilog. And some of the finer folk want to do VHDL, but that's too hard to achieve.

Well, but let me give you an example of a success story. So at Google, I worked on one of these machine learning chips, these TPU type chips, which some of you might have heard of, or that power machine learning algorithm, is that right? And that was a chip that was done using functional programming. The entire chip was done using this language called BlueSpec, which is a Haskell-inspired language for hardware design.

you know, develop ideas from people at MIT, maybe at CMU, and then a company was formed and BlueSpec, and we knew how to use BlueSpec. So we decided to just from scratch, from zero, make a new chip for machine learning, and we're going to use BlueSpec. And we did a whole chip.

and this chip needs a compiler, and the compiler was done in Haskell. And this was done very quickly. We made a chip and it came back and it worked first time. And it was done in a very, very short amount of time. The compiler worked incredibly well. And I think functional programming helped in many, many ways. So one way in which it helped was in the design of the chip. And I think one of the biggest things you have to get right about the chip is you have to build the right chip. You have to produce the right architecture.

Because if you don't use right architecture, you then go down a very, very long path. You know, it could take years and realize you've built the wrong thing and then it's too late. So an error at the design level is millions of dollars, right? So you want to explore the design space and get the right trade off because any chip that

that you make is an economic trade-off. You're making a chip because of economics, because whatever you want to do doesn't run fast enough on a processor. So you're already in an economic game. So then you have to know what's the memory bandwidth, how many parallel computation elements does it have, how many memory ports does something need? And so it's a big design space. So you have to get all these

all these values you have to, I think, as good as possible for the kind of things that you might want to run on it. So it's this huge design space. And what BlueSpec let us do is produce a parameterized description of our chip where we have parameters that describe all these axes that we care about to do every number of vector lanes, the size of the multipliers, the delays here. And we could just unfold in origami style

a high level of abstraction, gazillions of points in the design space, do a quick evaluation of each one, approximate simulation or whatever, or abstract interpretation, whatever, and pick the best candidate. And then that's the one we pick to then drill down and then spend a year and a half to get all the way down to it.

down to transistors. That was a huge value. This is agility of thinking and of exploring design space and looking at alternatives. And had we done that in system Verilog, one of the standard host languages, we couldn't have done that. Those languages don't provide you with the higher order, generic, parametrized, polymorphic way of thinking that you get from a Haskell blue spec way of looking at things. So I would say that's one advantage.

that we clearly got on that ship that we get from thinking functionally. I think another advantage we got is composition. It goes back to things I've said earlier, which is often it's something the hardest things to do are composition. You design things independently and they work independently. Then you put them together and they don't work. And often it's like,

It's just normal hardware. You design block A, it works. Put the waveforms in, the waveforms come out, works as you think it should. You design block B, you put some waveforms in, you get waveforms out, works as you expected. You put A and B together, why have I got a deadlock? Why am I computing the wrong, why is this matrix multiplier giving me the wrong kind of result? So it's the protocol of communication thing, path.

where things go wrong. And there I think BlueSpec, this wonderful Haskell hard script, which gives you a great advantage because in software we have a form of composability that we don't really form, that we have in hardware, because the hardware has this extra kind of extra time

And it gives us, it lets us independently implement and verify blocks. And then when we compose them, the composition works as we expected, because you can interface, you set an interface, when things are ready, when things are enabled. So there's this extra level of support for composing things together.

So you pay a cost for this because then you might not know how many cycles it takes for you to get your answer, but you get a composition that works. So in your life, you get nothing for some people who want something for nothing used to get nothing for something. So in this case, you get compositionality and you pay for it with latency or unknown kind of latency. And that seems like a great trade off, but then we could have people that separately design these blocks and then we put them together. Is there a chip where they came back, worked first time, which is amazing.

many times don't work when they come back first time and then you have to debug it produce a new mask set have a respin it could cost you a million dollars so that was like a great advantage that we got this ability to independently define blocks compose them to high level of assurance at the digital level that the chip work which chips can feel in many ways right even if the chip is

digitally correct, it might be incorrect at some other kind of electrical level, but things worked out for us well. And then I think we had a very...

do an implementation incredibly quickly compared to system Verilog or VHDL because we just had, we could just code the right level of abstraction for each block. We had the right types and we could operate with these types and form the right combinators to be able to reason and compose with these types and verify them and communicate from one engineer to another engineer what these types are doing. And then I would say another kind of advantage we've got, which is maybe not a technical advantage is, you know,

The kind of people that get excited and enthusiastic about writing Haskell and BlueSpec, they're usually very good engineers. They're usually very, very clever people. For me, that's the high order bits of someone. It's not, are you a great Haskell programmer or BlueSpec programmer or hardware engineer? It's more...

are you a great technical person? Because if you're a great technical person, there's lots of things that you can do. And in this project, we hired Haskell programmers to work on the Haskell compiler, and they worked with great people like Leonard Augustine and so on. They had wonderful...

And they were writing models to model bits of the hardware. And then when they got to know which were in BlueSpec, so it looked familiar to them because we use the Haskell dialect for BlueSpec. And then they just gradually transitioned from working in a model to working in a hardware. Move this register from here to here, add a multiplex there. And before they know it, they're a hardware engineer. So we did this kind of sneaky bait and switch on our Haskell programs to turn them into BlueSpec hardware engineers. And some of it went on to be like brilliant hardware engineers.

brilliant, did so hardware engineers. Some people came in as C++ ACs and they just had the right brain. Their brain was able to flip into being Haskell programmers and be productive. Not everyone, some people cannot do that. I had a friend who founded a company in Cambridge that went on to become very, very successful and acquired and now runs a vast chunk of internet.

He's a professor at Cambridge and he wanted to hire the best engineers he possibly could. But what he did was he advertised for OCaml programmers and people came and they interviewed in OCaml and they hired the best OCaml programmers. And when these programmers turned up for work on the first day, he said, "Great, you're working on the ZEN hypervisor. You're going to write in C from now on." So for him,

He didn't want to come up with programs. He just wanted the best engineers. The filtering process was hire the best OCaml programmers because they will be great C programmers too, because they're just great programmers. It's like a huge bait and switch. You've got these brilliant engineers that did this amazing coding, C coding on the Z hypervisor, which went out to be hugely fantastic because he understood.

That is so funny. If you work for a great outcome. Why do you think that happens? Why do you think functional programmers are just such great developers? I mean, I don't have a good answer to that. I mean, I would have kind of flippant...

I think maybe something about dynamic range there, right? To be able to think about abstractions, but also to be able to think concretely about economics of computation and being able to connect all the dots between them so that you're doing this progression, right? From being a mathematician to an engineer, but you kind of have this kind of an elegant model of how to describe something, but also you have not lost,

control over cost over megabytes and seconds. So I think that's partly to do it. Yeah, I mean, maybe it goes a little bit back to why I got into functional programming, which was, because I did talk functional programming as an undergraduate

I got interested in this myself because the BBC microcomputer had a Lisp interpreter and I was using it. So I also came with BCPL. So for fun, I was trying to write my own Lisp interpreter in BCPL. I was like a third year student at the time of a four year degree. And I was asking my compliance lecturer, David Watt, who was well known for Ada, books in Ada. He said, we've got this new lecturer who's around here called John Hughes.

He's installed this thing called Miranda. Go and ask him. So I start knocking this guy, John Hughes, his door, say, hi, I'm writing this Lisp interpreter. I'm writing it in BCPL, blah, blah, blah. And he looks at me pitifully and says, well, Satnav, it's good that you tried to write that Lisp interpreter, but here is the path to the Miranda interpreter. Try using that instead. So I got into Miranda and I did my final year project. I wrote a wee functional language for hardware design, compiling it to gates. And I had Mary as my finalist.

final year architecture lecture and when i saw miranda it felt like magic to me like it recreated the magic that i saw when i saw bbc basic so unfortunately that magic got extinguished from the compiler courses i'd done i'd learned too much about how your program gets compiled and run and the magic was all gone because i thought i understood how computers work

And then I ran Miranda programs and realized, no, actually, I don't understand how computers work. What on earth is going on here? How can I have this thing which looks like an infinite loop, but yet I can just take a few values, take the first 10 values and it gives them to me and things like that.

And it just sparked a new fascination with programming languages, you know, and how languages can model hardware with lazy evaluation. And I spent many years learning how functional programming languages get compiled and how GHC works and things like that. And I still don't understand all that. There's still some magic. There's still kind of magic there, but

I love this end-to-end thing. How do you go from quite abstract things to quite concrete things and connect up all the dots? Because what I value in the world is, I think the world has got too many situations where you've got a low-level thing for a low-level job, an assembler or C for a low-level code, or a high-level language for a high-level thing.

like Java for writing a web server. I think what the world needs are high level things for whole level tasks, because you're doing a little stuff is hard. You want to increase your productivity. So all these things I've worked on, things like Lava, there's Lava DSL. Lava DSL is not about making it easy for software engineers to

do hardware. No, you already have to be a pretty expert hardware engineer to get a value of Lava. Lava is this Bosch power tool to make experts more productive at being experts at what they do and be able to do it quicker and easier into a higher level of assurance than they could have done otherwise. So I think we need high level tools

more high-level tools for lower tasks. And that's what I think is like Haskell, Camel, and Coq are all like super important things. I want to use these things for low-level things. That's why we use Coq to do hardware. That's why I love what Adam Cipalla does with Coq to Gates. That is amazing. What are the kinds of safety guarantees we're interested in when we are talking about hardware? So...

Often in protocol, you want to know that if you make a request within 10 cycles, you get some response or some error acknowledgement. And if you don't, then something's gone wrong, right? There's some kind of bug. It's kind of bugging the system. So often there'll be, I think a mixture, you know, it can be stronger within five cycles. The output should be A times B. You can write things like that. But it's often...

I think a lot of very useful properties are like bad situations you never want to be in. So they're kind of indirectly, they're also like somehow specifications, right, of your system. So for model checking, right, those are quite useful. I mean, you can't use model checking to check all kind of properties, but there's a whole range of kind of safety things that model checking is very useful.

it's very useful. There are other more far more complex properties and for those who are driven, you'll be probably forced in the path of model checkers. But I think the kind of things we can check automatically just improves every year as the capacity and capability of systems like Z3 and so on

important i would say you know i mean the high level answer to your question is like protocol kind of thing so this happens and this other thing happens there within the other end cycles this this thing should happen or this other thing should not not happen yeah

Well, one question that I usually like to ask my guests is somehow how they see the future. So in your case, how do you see the future for hardware verification? Where do you see, you know, the current mainstream is headed at and where we still...

developing new ideas and what are the points, the pain points that we should improve and what would be maybe the best case scenario for formal verification, for formal verification in hardware.

At the moment, I mean, the current situation, I think, is pretty good in some ways, because I think actually the hardware world is leading the software world in the use of your LTL-inspired property checking of hardware. I think that's been a huge success in the industry. It's part of the standard language that people develop hardware and system very long. And there's commercial ecosystem tools from Cadence, from Synopsys, from Enter Graphics,

but very powerful models checkers, as well as the TabbyCAD, the OCCQ software as well, which is what I use at Grok. So that's kind of healthy, but that's a stepping stone. We talked about checking properties. I would love to see total verification. I would try a complete spec

and prove that this entire pile of gates conforms to that complete spec. And there, we've still got a long ways to go. There's been great work already of people using theorem provers like Hall-Lite, like at Intel, the work of Harrison and so on. I know that theorem proving gets used for hardware. I'm guessing, you know, to some degree at Apple, maybe at some other companies as well. And I think, you know, maybe the next,

Another great battlefront there, I would say, is the work of Warren Hunt at University of Texas. So they have this system, ACL2, which I think is just like an amazing tool with phenomenal verification capabilities, which are very practical and very well maintained, and the software's engineered to a very high level. So for people who want to think about or want to work on this as like a research problem, as a research area, or if you work on chips, you want to go beyond

Jasper Goad type kind of verification. What's the next thing you can look at? I would strongly encourage you to look at the ACL2 system from Warren Hunt. Just go to Google Warren Hunt University of Texas and you can follow links and find out more things. He spearheaded this conference, FMCAD, for many years.

We just published papers on a practical form of verification for hardware. So the papers, you read some of the recent papers there, you'd get a good idea of where is formal verification right now for hardware and where is it heading? So I mean, I think it's in a good state and it just keeps

improving more and more. And it's becoming more and more a standard part of how chips are specified and designed, but we're still not there yet. Well, that sounds really good. Well, I think I have covered everything that we have thought about. Is there anything else that comes to your mind that we didn't have the opportunity to discuss or something that was maybe left out?

behind and didn't get as much attention as it should. I don't know. Nothing immediately comes to mind. I'm very happy to answer any arbitrary random question. But I guess one thing I would like to emphasise is how valuable it has been to have

to be trained in the world of programming languages, to have been a PhD student in a programming languages group and to have gone on and do PL inspired kind of things. Because I know everyone who's either thinking of doing a PL, PhD or is currently doing one or whatever, to think that they have to go and be a PL professor or go and work on LLVM, a company or whatever.

I think studying programming languages, it gives you a mental toolbox about how to think about problems, how to structure them, break them down, solve them, categorize them, investigate them, describe them. So it gives you a philosophy of how to think, tackle problems, which is broadly applicable to so many different areas beyond just core PL. And I mean, and I think all the things I worked on, whether it's, you know, hardware, designing hardware circuits,

and verifying them, writing Java code, optimizing bytecode on Facebook, aspects of logging at Kubernetes, whatever. They all come from this school of thought and discipline perspective about how to look at the world and how to solve problems. So I would say that's what's really valuable about the wider PL and PL theory kind of world. So no matter how narrow a field or what you're working on, you might think you're working on something that's narrow and esoteric,

and the skills you're developing, maybe you'll never be able to use them in what you do next. I think that's a false thought. I think there's just a broad bunch of skills and problem solving skills that your neurons are developing by this. And I would really encourage people to think about PL as a kind of a research area and as a community. And I would say, and I think it's a great community. I mean, I've worked in several communities. It's my favorite community.

And I've got people who are colleagues who are now my friends and they come to my house for dinner. I've got conferences, we go for dinner, we go for drinks. And I love seeing them. And I've always loved them for their technical abilities. I know I love them for the people. And there's come my wider family. And I think that's a wonderful, special thing that you get by being in a...

community like PL because you then form this network of friends and community that transcend the current company you're working at or the current university you're at. And I think it's a great opportunity. Not everyone has that. Often, I've noticed for myself when I've worked in product group jobs, you've got some people who you think are your friends and then when you move from group within the company or you move to another group, you never see these people ever again. A lot of these relations are very transactional, but I think

when you're a member of a research community, you have a chance to form these professional connections and some of them which then turn into your personal kind of friendships. That's been, I think, a great valuable thing to me in life. I love the fact that I'm going to go to PLDI in a few weeks time. I'm going to have dinner with Derek Dreyer

of Alistair Donaldson, Andreas Rosberg, and all my other friends here. That's like a great source of strength. And these people are inspiring, even when they're talking about what they're going to order for dinner or when they're talking about what they've done in Rust or whatever. So I would focus on that, right? I would definitely...

think about the community aspect of being a researcher and whatever, whether it's PO, whatever community is, and to try and think about nurturing that and trying to develop that and trying to be part of that, right? - I definitely agree and I relate to that. I love going to conferences and seeing your old friends again,

But this idea where, you know, learning functional programming, learning programming languages ideas, it's something, especially in the current curriculum of computer science, is something that often enough is widely overlooked. Right. So I had a friend this last semester that she was about to graduate at Purdue. And then I started 10 years all about programming languages, about Curry-Howard isomorphism, about functional programming languages.

And she's just like, I have no idea what you're talking about. Where is all of these things hiding from our curriculum? And I'm like, well, you could take programming languages class with my advisor. She's like, okay, sign me in. And then at the end of the semester, she was like, dude, there's this completely different world of computer science that I had no idea. You know, I'm just a completely different, she could see programming languages differently.

well, she could see computer science programming in a completely different lenses, completely different view, which I find absolutely fantastic, right? Because it's a cult and it's a great cult. You should join it. It is. Let me say a bit more about your conferences and see my friends having dinner. I also want to emphasize to anyone who's listening, who sees me at a conference, come up, say hi, come for dinner, come for drinks. Because I want to meet everyone. I want to know what everyone is doing.

I got into dinner at that conference because I felt excluded. I remember the first conference I went to in '93, '94 in Napa Valley to do FPGAs. I turned up at this conference, I gave my talk, and in the evening, everyone disappeared into their cliques. There was no banquet, whatever.

And I'm standing in the Marriott Napa Valley on my own, sitting at the bar eating popcorn. This is a bit miserable. Why am I not in a clique? So next year, we went back and thought, okay, well, if I can't join a clique, I'm going to create a clique. So I came back and I came up with my idea. And then his girlfriend, Susan, so I said, Susan, can you go to Napa Tourist Board and get a recommendation for a restaurant? Book a restaurant for 14 people or

And then I went around a conference and I randomly invited people. And I wanted to specifically invite some people at the establishment, some people from industry, some people from research. And then deliberately I wanted to invite postdocs and PhD students, people with some stories who might also not be in any kind of clique. I got this mixture of people and we go to... And in the evening we rock up this restaurant called Domaine Chandon and we turn up. There's quite a big

fancy looking restaurant with waterfalls and big grounds. And we turn up and actually it's a very fancy restaurant. We fancy that, I normally go to, because it's a restaurant with this famous winery, Shandong. We turn up and the gentleman at the door says, "Well, welcome to the restaurant." We do require gentlemen to have jackets. Now of the 14 of us, only one of us was wearing a jacket and that was Susan.

And so the, but this gentleman said, "Don't worry, we have jackets." So for the other 13 of us, they gave us jackets and we all sat down. One of my colleagues, this guy called Tom Kean, he worked at the Xilinx Edinburgh company, a fellow Glastonburyian. I can't exactly do his accent. He said, "But this jacket, it doesn't fit me." And he said to him,

don't worry, sir, you don't need to wear the jacket. One just has to drape the jacket over the back of the seat to which point 14 engineers and computer scientists say, but why do you just preinstall the jackets on the seats so we don't need to bring them? So we have this fabulous dinner, which is amazing, mainly seafood to go with champagne. And then the bill comes and it's astronomical. And I thought,

Damn, here I am trying to ingratiate myself to this community so I can become part of it. And I've just blown it by inviting people to super expensive meals. So I did this negotiation. I said, "You work at Intel, this is a student at BYU, so could you cover half the cost of their meal?" So I did all this negotiation to try and even out the spend so the industry people compensated a little bit for the cost

of the academics that all kind of worked out. The next year I was in a program committee. That's when I learned the importance of like networking, getting to know people, just going up and talking to somebody if you don't know them and say, "Hey, come for dinner," or, "Come for a drink," or whatever. And that process of negotiation and so on

I've met and had dinner with people, got to know people. But then I also want to make sure that people are not excluded. So whenever these, like when we plan these dinners, I always try and, I'm always going to look out for who else can I invite that I don't know, or a new PhD student or someone that's new to the field. Because what you want to avoid is having cliques where the same people are going to have dinner at the conference of the same other people. You have this fixed point and there's no progress, right?

That's why I'm very, I will say whenever I go to conference, I usually tweet people around saying, "I'm going to be at ICFP. If you see me, come up and say hi. Let's go for a drink. Tell me about your research, what you do." I'm really, I'm very happy to talk to anyone and everyone.

and i think the real community i think he's done you know a good job with sync plan mentorship so i've been a sync plan mentor to several people i found it really fulfilling i i hope that the mentees have as i just saw one of them at the nasa public methods conference just just just the other day so this i think there's a lot of great ways to also give back to the community as you

at all stages from even when you're a speech teacher to postdoc to early academic and I would really recommend it. I think it's just a fulfilling and rewarding thing to do and it's just one more way you can interact with other people so look out for all these single plan mentorship opportunities and all these special lunches to do with various topics and various groups of people with common interests and I really encourage people at these special single plan conferences which I'm

I'm familiar with, really try to take advantage of it. There's lots of wonderful people who create and drive these things that try and nurture a better community and also try to address some of the structural problems and failures in a community and in a wider society and find ways to try and counter them and address them the best way we possibly can to make it a welcoming and inclusive society as we possibly can. Yeah. Yeah. No, I definitely agree with you. I love conferences so much. When we go to, I think we went, oh, what?

When we go to conferences with, and I have my friends from university, I always, you know, like we always end up naturally being together, right? Because we know each other. And then at some point I look at all of them like, guys, what are we doing here? We need to meet new people. This is the great part of the conference is going out and talking to people. So I just randomly start walking and find someone I don't know and make some random conversation. And I tell everyone to do that because that's the time to meet people. That's the time to network.

And that's why we're there. So everyone, it can be a little uncomfortable, especially if you're more introvert, but everyone there will be open. Everyone there is there to meet new people. So definitely just walk up to us. Yeah, I think conferences have many failure modes. And I think one is conference banquet, just something I'm not keen on for many reasons. One is just because I have celiac disease, there's always nothing I can eat at a conference banquet.

or I have to eat the lowest common denominator of what I could eat, what Benjamin Pierce could eat, and what Adam Chappelle could eat, which is, I think, tofu with a wet salad or something like that. So I hate conference banquets because people often...

sit with people that they know, or maybe a few other. And then you have to have this, I mean, we're computer scientists, and we take 300 people, and we try to synchronously serve them the same meal at the same time through broadcast. That's just completely nuts. That doesn't match the economics of how a kitchen works. You feel qualified to write a paper at ASCOS on computer architecture. Completely nuts, right? So I think we should just do away with conference banquets. But what we should do instead is, we have a

conference, book 20 restaurants, randomly allocate the people who come to the conference to all these restaurants. I mean, adjusting for your dietary restrictions. And then you're going for dinner with five other people at night. You don't know who they are. And you could not go if you're a pervert. That's why. But if you turn up...

you've got five other people that you probably don't know exactly right you can talk to and you can talk about technical things you can talk to about the food you can talk about how you got you could talk to me about music or whatever i think that would just do wonders for shaking things up and especially for people who are new to the field or or maybe a bit shy or whatever connecting with the established people because you so much of your life is done by opportunities and

who you meet and who you know and who you can express yourself to. So your personal and social dynamics are just a huge part of that. And I think it's important for people to be, for emulsification to occur, right? - Exactly.

Oh man, I'm looking forward to meet you in person in some conference in the hopeful near future. I'm going to a bunch of conferences in September. Are you only going to the, you said, ICFP? I've already been to ICFP. I was going to go to ICFP, but I'm not going to go anymore. I'm going to PLDA instead for... PLDA. ICFP I regard as my home conference, but due to

- There's just tragic reasons. I'm gonna go to Cambridge in a couple of weeks. So there's a reason I need to be there. I can't afford to make two trips for a PL conference. So the PLDI is immediately after the event that I need to go to Cambridge. So I swore I canceled the ICFP then. - Okay. - Even though, yes, the graphs and charts conference, I mean, it's not graph charts anymore, right? PLDI and ICFP have come much closer together in focus.

So I'm going to go to PLDI instead and look for restaurants in Copenhagen rather than Milan, which I feel a lot better about. LAUGHTER

This is going to be my first ICFP I've ever been. My home conference is usually Popple, so I'm very excited for that. That's how it goes. Did you go to Popple in January in London? Not London, not London. The one before that was New Orleans, so I went to New Orleans. That was awesome. Yeah, I was at a London Popple, which had a great slew of restaurants. I wish I could go, but I was busy writing my master's thesis and I didn't have money, so...

I don't usually go to Popo. I went to this one because I was in the programme committee for Popo. Ah, cool. In the past, I used to be on the Singapore steering committee, so I also went to Popo back then because we'd have a steering committee meetings. But if I can only go to one, I go to ICFP. That's the...

Where I feel at home. Where my tribe is. Well, we keep talking about that offline. Let me just close this episode real quick. So thank you everyone who stayed here with us today. Talking with Satnam was so great and heartwarming. He's an absolutely incredible human being. And I'm so happy that we had this conversation. Thank you so much, Satnam, to being here in the Type Theory for All. And I hope to see you again in the near future. Thanks for inviting me. I'm honored to be on the show. Bye for now.

♪

What an amazing soul. This conversation with Satman was so nice. I really, really liked it. I hope you guys enjoyed it as well. I sure learned a lot with him, with his experience. What an incredible person. And I can't wait to meet him in person. Unfortunately, he will not be in ICFP. I will be in ICFP in September in Milan. I think it's September 2nd. So if any of you guys are listeners will be in ICFP in Milan,

hit me up. I have a surprise for you. The first five listeners who reach out, I will have a very special gift related to the podcast and related to our content. So if you're going to be there, hit me up and I will make sure to bring your gift. Other than that,

Don't forget to join our Discord. We have that study group that I mentioned at the beginning of the episode. We are learning Coq through Software Foundations. There are two amazing volunteers making that a possibility. So go to our website, typeT4L.com, join the Discord.

If you have any questions, any comments, if you're liking the content or is there anything that you dislike, send us an email. typetheorforall@gmail.com. I take emails that doesn't necessarily have to have a name or anything like that. So if you have a complaint, you have a rant. Although, you know,

you guys are surprisingly nice people maybe it's because i maybe i've i've only seen those trolls on twitter and youtube people can get pretty mean and just because i opened things on on email then maybe the trolls keep away but i am i really appreciate all the support talking about support if you are able to and have some spare money to help us out because currently i'm quite unemployed you guys know this already so if you can go to our co-fi platform all the links are in the

This podcast was edited by Play Audios.