Recorded 2024-11-15. Published 2025-03-17.
In this episode, Andres Löh and Mike Sperber are joined by Farhad Mehta, a professor at OST Rapperswil, and one of the organizers of ZuriHac. Farhad tells us about formal methods, building tunnels, the importance of education, and the complicated relationship between academia and industry.
Andres Löh (0:00:18): This is the Haskell Interlude. I’m Andres Löh, here today with Mike Sperber.
Mike Sperber (0:00:22): Hi.
AL (0:00:23): Our guest today is Farhad Mehta, professor at OST Rapperswil, who many of you might know as one of the organizers of ZuriHac. We’ll be talking about formal methods, building tunnels, the importance of education, and the complicated relationship between academia and industry.
Yeah, so with us today is Farhad Mehta. Welcome.
Farhad Mehta (0:00:43): Good morning, Andres.
AL (0:00:45): Our first question, which I’m also going to ask this time around, is typically how did you first get into contact with Haskell?
FM (0:00:54): Oh, wow. Maybe it’s better to just have a – no, I mean, maybe it’s better to just talk about how I got into my first contact to functional programming, which then led me to Haskell.
AL (0:01:12): Yeah, absolutely.
FM (0:01:14): So, I remember as a child, I was really fascinated with the programming. And at that time, I think like many more of us in our generation—now I’m outing myself out here—I had one of these Commodore 64 computers, and the only thing you could program with one of those was BASIC. And as a child, I was really somehow very excited by this notion of programming this machine using some language, and it was basically like love at first sight. And that led me into this area of computer science. And I was thinking that, yeah, basically, it’s so cool. I can do everything I want with it. And that was until I started my bachelor.
So when I started formally learning what computer science was, my first introduction to computer science was basically a course in Scheme along the lines of the Wizard Book—Structure and Interpretation of Computer Programs. And I was in India a very long time ago, and that just blew my mind. And in the beginning, I was thinking, “This is a bit strange. This looks nothing like basic. What are these people talking about?” And then at the end, I was thinking that, wow. I mean, after like three or four weeks, I was thinking that, wow, this has so much power. And that basically led me to functional programming. And the first time I even looked at something like Haskell was my Programming Language course at that time. So that was at IIT Delhi. I think a number of people in this community came from there, which is also something great because it also emphasizes the role of teaching in this. I think if our professors didn’t really have this mindset, we wouldn’t be in this area either. So at that time, it was Sanjiva Prasad, S. Arun Kumar, Subhashis Banerjee. These were the people who taught me at that time. And it was in my Programming Language course that we had a first glimpse of Standard ML. And I was thinking, “Wow, this is like Scheme, but has some safety belts on it.” So that was really great as well.
And so that was my first experience with an ML-like programming language. And everything after that, I mean, once you know Standard ML, I mean, everything else in this area is just one little tweak away. So then I spent some time at Project Cristal at INRIA, where they made the OCaml compiler. And yeah, the love affair went on.
And Haskell, actually, I came in quite late with Haskell because I spent some time in industry, and unfortunately, I had very little exposure to Haskell and functional programming. And then I remembered two points of contact. One was at the ETH when I was teaching, and we had a course. So my professor and I started a course in formal methods and functional programming. We thought it would be a one-off thing, but it’s still going on right now. And so there, someone taught functional programming, and he chose Haskell for it. So that was my first sort of when I heard this name even. And my actual real starting point with Haskell was basically when we started ZuriHac at my university a long time afterwards, and they said that, “Hey, would you be interested in hosting this conference?” And I was thinking, “Yeah, sure. Let’s do that.” And I basically learned it at ZuriHac, to be honest with you. It took some time, though. It was not as simple as I thought it would be.
AL (0:04:39): Yeah. So it was hardly your first exposure to functional programming at that point.
FM (0:04:45): No, no, no, no.
AL (0:04:45): So, the way you’re telling the story is that programming was love at first sight. And then you got into contact with Scheme and later Standard ML, you’re saying, during your bachelor’s.
FM (0:04:59): Yeah.
AL (0:05:00): So I think that’s common for many, but it’s not necessarily the common reaction that people say, “Yay, this is even better than whatever I’ve done before.”
FM (0:05:10): Yeah.
AL (0:05:11): Quite a few people are saying, “Oh, why should I learn this academic nonsense?” So, you didn’t have that reaction. Is that because you had great teachers or –
FM (0:05:21): Yeah, I think the reason was – and my first reaction was that, right? So my first reaction was, “This is really strange. All these brackets, what’s happening?” But this lasted for like three weeks. And I must say there was some amount of negative publicity that was happening.
I remember when I started my university course, there was a choice. There was a choice between Introduction to Computer Science. There was one course of that, and there was something else called Introduction to Computers or something like that. This was another course. And the basic idea was that if anyone had very little exposure to computers in general, they would take the other course where they’ll talk about Pascal, and this is how you switch it on, and there’s a CPU and all that sort of stuff. And since I already owned a computer before, that was criteria enough for me to join the advanced course at that time. People used to tell me, “Hey, the other course, the one that we learned Scheme, that’s a bit advanced. Just lie and tell them you have no experience and just go into the other one.” And I thought that, “No. I mean, let’s see what this is.” And my initial experience was that, well, okay, this is a bit strange. But after you get a little bit of a hang of it, I thought that, “Oh, wow. Okay, this gives me a lot of power that I didn’t have before.” And I think that is this initial hurdle that people face.
Unfortunately, it’s because a lot of the – I mean, this is my personal opinion. A lot of the initial material that people normally have is in this area of programming, in this—I don’t know what to call it—quick and dirty style. And they think that, “Oh, I can achieve so much with so little.” But they don’t really see that, okay, you can have fast gains, but it’s not really getting you anywhere. And I think that is what a lot of people struggle with when they start learning out a program, in my personal opinion.
AL (0:07:18): I think that’s very interesting because I think it’s slightly different from the argument I typically hear. So I think if I try to recap what you’ve just said, as you’re saying, that a lot of introductory programming material and other languages is focused on sort of quick and dirty programming and achieving as much as possible. And sort of as little time and not a lot of stuff, by contrast, is paid on sort of what is maintainable, robust, scalable, correct programming, and that serves as a disadvantage for functional languages.
So the thing that I’ve heard more often or thought about more often myself is that a lot of introductory functional programming seems to be very self-centered in the sense that you’re often like teaching functional programming as a different thing. But then what are you teaching? You’re teaching about type systems, about logic, about sort of higher-order functions, not about getting stuff done.
FM (0:08:17): Yes.
AL (0:08:20): And so, I mean, perhaps there is no real contradiction. Perhaps it’s just two sides of the same story?
FM (0:08:27): I think this is a very interesting thing you’re pointing out, Andres. I also have this opinion. This first course that I talked to you about, it wasn’t called Introduction to Functional Programming. It wasn’t called Functional Programming, or I don’t know, Scheme or something like that. It was called Introduction to Computer Science.
AL (0:08:47): Okay.
FM (0:08:48): I think maybe our field or people who think in this area maybe need to think about how we market or brand – I hate these words, but market or brand what we’re doing. I think that we tend to make it a bit too specialized. And I think that if we sort of say that, hey, this is not some niche; this is actually something that used to be part of the mainstream and should actually have a lot more exposure. I think that that would be a lot less counter to what we’re actually saying. I think maybe we, as a science, have maybe the wrong aims, or as a commercial, in the commercial sense, maybe the wrong aims. I think we value a quick and dirty, maybe a bit too much at the moment.
MS (0:09:40): So, it sounds like there was a progression from Scheme to Standard ML to Haskell.
AL (0:09:47): Yeah.
MS (0:09:47): Can you describe a little bit of what it was that got you to prefer the next step over the previous one? So certainly, you mentioned that there were safety belts with Standard ML, so that had some appeal for you.
AL (0:09:59): Yeah.
MS (0:10:01): The implication is that Scheme does not have safety belts.
FM (0:10:04): That’s not what I wanted to imply. I’m sorry about that.
MS (0:10:06): No, no, that’s okay.
FM (0:10:08): So, I think the honest answer to that, why did I do something at the next level, is basically a very lazy answer. It was basically a coincidence as to what I was exposed to at the next time. Scheme I got exposed to because that was what was in the course. And it wasn’t really centered on Scheme; it was centered on learning how to program.
The second one was a course on programming language, so the Standard PL course. And that was done with Standard ML, and so I learned Standard ML, and I learned to like it and love it. And the next thing was that I had this opening at INRIA where it was OCaml. So I was basically in touch with OCaml. And Haskell was basically, someone came up to me and said, “Hey, would you like to host ZuriHac?” And I said, “Yeah.” But maybe it would be nice if I learned Haskell also. And so, it was basically a coincidence. I wouldn’t really say that I seeked it out. I basically just went with the flow. I’m sorry.
MS (0:11:09): But it’s not as though you appreciated the benefits of static typing, right?
FM (0:11:13): Yes. Yes.
MS (0:11:15): So it’s okay. So full disclosure for the people listening. I was once editor of the Scheme standards. I think that’s why Fahad is a little bit hesitant to dunk on Scheme. But feel free to do that anyway.
FM (0:11:26): And I don’t know. I think that it’s been some time since I’ve – I mean, it’s been a lot of times since I’ve looked at Scheme, but there are many things that I did appreciate quite a lot. And I don’t think that there is a natural – I don’t know. I wouldn’t like to see it as some sort of competition in these things. I really think that it’s the same mindset in a different form. I don’t really think that there’s a lot of – I could see myself writing Scheme code again, very happily again. And so, yeah. And a lot of the people I know and respect and like to talk about are in this area. So it’s not all this, like all the strange loop people. I mean, crazy stuff, crazy stuff. And yeah, I have a big respect for this area as well.
AL (0:12:27): I would still be interested to follow up on Mike’s question, like with the step between, say, Standard ML and OCaml and then Haskell. I mean, would you – I don’t necessarily want you to say that you think Haskell is better because I’m not even sure that it is, but for you personally, what were your different experiences with the two? And say, if you were to pick a programming project now, is there a preferred language you have?
FM (0:13:00): I think I would be the wrong person to ask about a programming project. Of course, I have my opinions. But since I haven’t really been working in industry with a functional language for some time now, maybe I wouldn’t feel free to answer this. What I can say, though, is that what would be a good language to learn this style of thinking in? And there, I think that Haskell would – it was my choice because it has a certain sense of purity and is closest to the ideals of this way of thinking. So I thought that it was the best vehicle to teach this way of thinking.
Practically, there are lots of other things that come into play with this. There is performance, there is a number of people who are comfortable using it, there’s acceptance in the industry—all these sorts of things come into it, which I think that I’m maybe not the best person to answer. But in my current line of work, I think that I’m quite happy with Haskell as a language, as a vehicle to teach this form of thinking, because I think it hits a sweet spot. You can actually do stuff in it. You can actually program in it for people in the area where I’m teaching. I have a functional programming course for second-semester students. And I think that I know doing something in Agda or something at that level, I would maybe lose my job. And so I don’t know.
AL (0:14:40): Job safety that bad.
FM (0:14:42): Yes. Yeah. You’ll think I’m totally crazy. But I think that there is a sweet spot there. It’s as closest to the concepts as possible without being something esoteric. Of course, opinions of this may be divided. And at the same time, it’s pure in the sense that I can’t do funny stuff like write a print statement somewhere. And that forces people to really go through it. As a language, it’s quite minimal. I mean, I remember the first time I asked my class, what language would you like me to use for this? And we are in Switzerland. So many people just said Scala. And I said, “Okay, I’ll use Scala.” And I said, “How different can it be?” I was quite naive at that time. Just came to university from industry for some time. I was thinking functional means some ML style or some Scheme or Lisp style language. And I said, “Okay, I’m going to do Scala.”
And so I remember the weekend before my course started, I was thinking, “Yeah, okay, let’s take a book and start doing my examples.” And then I looked at it and I was thinking, “Oh my God, this is like a huge piece. This is like a complicated language.” And I basically gave up on that, and I did it in OCaml. My first run of the course was an OCaml basically. But yeah, I don’t know. What was the question? Sorry, Andres.
AL (0:16:14): It’s no longer important what the question was. I actually have a slightly different – I mean, I want to talk to you more about the current teaching and so on, but before we get completely lost on that, you mentioned several times now that you had a time in between where you worked in industry and then you went back to academia and that in industry, you didn’t have much exposure to functional programming. Did that play any role in your decision to go back to academia, or was that for completely different reasons? Or can you say a little bit more about what you did in industry?
FM (0:16:48): Yeah, definitely, definitely. Yes, let’s maybe back up a little bit. So why I went to industry, what I did in industry, and what I did from – so what I did after my affair with functional programming was that, as many functional programmers or many people who are hardcore in this area of programming languages, you sort of think, “Okay, what’s the next kick?” So, you’ve done ML, there’s OCaml, there’s typesystems. You read Benjamin Pierce’s book, and you think, “Yeah, okay, what’s the next step? What’s the next step now?” And for many people, the next step is basically a theorem prover. What else could it be?
So basically, I had quite a long stint with theorem proving as part of this Isabelle/HOL group in Munich and all that. And then that led me to do my PhD at the ETH, where they were actually looking for someone to design the proof system for this event B language, which is – I don’t know. It doesn’t have a lot of international exposure, but in France, these sorts of things really get used. And I was thinking, “Yeah, okay, this would be really great.” So I was in this area of logic and basically moved away from functional programming for quite some time. And so I was in this logic/theorem proving community for some time. And that was my PhD basically. And after that, I was thinking, “Okay, what do I do now as a job?” Because at that time my partner was still studying, and we were thinking that it’d be nice if we stayed in the same physical place. That’s the thing with academia. You basically have to move whenever you change. And that was frustrating for me because I’ve already moved quite a number of times.
So I was looking for a job. So, like a real job. And in the alumni paper at the ETH, there was a job ad for the startup, which was doing stuff in the area of railways. And I was thinking, “Maybe they could use something in the area of formal methods, functional programming.” And so I applied. And the boss and the owner was also did his PhD in so formal methods-related stuff. And so there was an instant connection there. And he told me in the beginning also, “Hey, we like this sort of work, obviously, but the state of the industry is something else, and you would have to program in Java.” And I was like, “Sure, I mean, no problem. I can do that.”
And so I went into this job with sort of thinking that, yeah, okay. I mean, at least to be in the company of like-minded people is good enough, even if the job is not really a hardcore theorem-proving/formal method job. That’d be okay. Funnily enough, every hard engineering problem I faced at that time sort of pushed the boundaries of what was possible at the mainstream. I can give you a few examples.
So at that time in Switzerland, there were these huge tunnels. There was the Gotthard Base Tunnel that we were currently writing the control software for, or helping write the control software for Siemens at that time. There was this Lötschberg Base Tunnel. And they sort of pushed the boundaries as to what was safe in train travel. So the Bundesamt für Verkehr, the Swiss travel, I don’t know, certification body basically said that, “Hey, the rules of safety don’t really apply for train travel anymore if your tunnel is now almost 60 kilometers long. So you can’t just stop in the middle of somewhere and just say, ‘Okay, I’m in a safe state,’ because there’s stuff happening all over the place. There may be noxious fumes around the place. We need some extra security measures, safety measures for such a tunnel.” And so they had a request for functions that were quite novel in the area of train safety, for example, that a train always has to have a designated safe escape if there’s one fault in the tunnel, for example. And the other one was that you needed to have a certain amount of extra buffer around trains and things like that, and this ended up being quite complicated.
And at the moment that these things came to my desk, I was thinking, “How do we even manage to do these things?” And even though we had to, at the end, program the stuff in Java, because that was basically what we offered and what they wanted, the logic behind it, I don’t think I would have been able to think about this if I didn’t have this exposure to this formal, systematic way of thinking about problems.
And I remember that time that it was just – of course, you could say that, yeah, functional programming, it’s really just an implementation. But the thing is that I feel it really shapes the way you think about problems. At least it shapes the way I think about problems. And I don’t think I would have got these things correct. I mean, it wasn’t just me. I had a really good master’s student who did his internship with me from the ETH. And he was basically in this formal methods/functional programming course as well, so he knew what I was talking about. And basically, we went through this whole problem in a very sort of systematic way, and we found out that, hey, this problem is a lot more difficult than what we thought about. And so I was thinking that, what about people who haven’t had this or who weren’t exposed to this way of thinking? How would they even go about thinking about this? And that really struck a bell with me, saying that, hey, this is something that should be part of mainstream curricula. It’s not something strange.
And so then after this, at some point, I decided to go back into academia, and it started in sort of an indirect way. So I was missing teaching. But one or two years, I was doing part-time teaching in Berufsschule. That’s like an apprenticeship Schule, school in Switzerland. And I really started to enjoy it, and I was thinking that, “Hey, I want to go full-time into this.” And there were personal things that happened at that time. Also, my son was born. I started working about 50% so that my partner could also work 50%. And then that led to me being free enough to take this part-time job and everything. And so that led to me doing this. And I was thinking that, “Yeah, I really like teaching.”
I had a colleague of mine who was working in the university I currently work at—at the OST. At that time, it was called the HSR (Hochschule Rapperswil). And he told me that, “Hey, you would be really perfect for this job because there are people retiring.” And I was like, “Okay.” And the job was actually for software engineering. So it was a professorship in software engineering. And I was at my Wahlkommission. They have a panel of people who say if you get the professor job or not. And I was basically, I don’t know, quite free with this because I already had a job. I had two jobs. And so I was thinking, “Yeah, let’s just try. Let’s take it easy and see what happens.” And I just said that, “Yeah, I know all the stuff in software engineering, but I still don’t think that this is what we should be teaching. This is not only what we should be teaching. We should also be talking about the systematic approaches to this and maybe something like functional programming.” And at that time, I was thinking that, “Hey, this may just cost me my job,” because if they think I’m some esoteric, I don’t know, person with these things. But they actually had a lot of trust in this, and they said, “Oh, really? Because we don’t have a course in functional programming, and maybe this would be something.” And I’m thinking, “Is this a joke? You really want me to do this?” And there’s like, “Yeah, yeah, it would be something.” And I was like, “Okay, cool. Then count me in.” And I started this.
So, even my move into teaching and working in a university wasn’t really fueled by the need to teach functional programming per se. It was more of a dissatisfaction with the state of the art in our science and thinking that, “Hey, it would be really nice if people had some sort of systematic way of doing things.”
MS (0:25:24): So you describe how you took stuff from your training in functional programming into your job in industry and how you then transitioned to your teaching job. Presumably, your industry experience helped you a little bit getting the job, but was there anything that the industry experience taught you that was worthwhile, valuable to you later?
FM (0:25:41): Yes. Nice question. Let me think about this. So my industry job definitely helped me get my current position. That was definite. What did it teach me? I think at the time I started my industry job, most of my time I was working in universities, and the way of working there is quite different. I think what I did learn in my industry job was, I wouldn’t say they were the soft skills, but I would maybe say the hard and dirty skills of the real world somehow. Yeah, I don’t know. I don’t know if this podcast is the right place to discuss this. I mean, things like, how do you negotiate a contract? How do you fix a price? How do you do project planning? How do you, I don’t know, hire people? When do you let go of people? These sorts of things. It was a nice – I wouldn’t say it was a nice experience. It was quite a traumatic experience if I’m honest about it. But it did give me a feeling for what the, let’s say, “real world” is like, and that was quite helpful. Especially when you’re teaching people who enter industry, it’s important to have the reality check there. And I think that was quite important.
The other thing that I really enjoyed in my industry job is to really think that, hey, the skills that we have as PL people and as formal methods, functional program, these sorts of things, they are relevant. It’s like people say that when you get into industry, these things are not important. And I think that’s a total misconception. It’s a total lie because, of course, if you don’t know what you can do with a nice systematic approach, of course, you don’t end up doing it, and everything becomes just another hack. And so those were the things that I think really helped me.
MS (0:27:43): So from how you described your job working on trains, it seemed that – and you did say that you worked with somebody who also at least knew of the existence and the possible value of formal methods, right?
FM (0:27:54): Yes.
MS (0:27:55): I mean, this is an often-discussed topic, but can you be a little bit more concrete about why that ended up not getting – I mean, you kind of had to do it undercover, right? You had to apply secretly your functional programming Kung Fu in Java code. But instead, the company that you’re working for could have just gone, “Well, safety is really important, important quality metric and software architecture. Formal methods is a way to achieve it. Let’s do it.” What kept them from doing it?
FM (0:28:20): Yeah. What made it being under the table? I think it’s the state of the industry at the moment. People are reluctant to take risks in this. I mean, it’s not a risk, but for most of them, it is a risk. It is a risk because other – I think many things that are maybe what we think is irrelevant come into play. For example, how many Java programmers can I hire fast? It’s not about the quality or anything. It’s just how many can I hire?
The other thing is also if you look at the norms in industry, I mean, the norms are written for – I mean, if you’re happy, if you’re lucky, it’ll be something like C++ in there. But think about something like Haskell or a functional – I mean, this is non-existent. This is non-existent. The big part of industry is not aware of our existence. Let’s put it this way. And so there, to come into this, it’s a big risk.
MS (0:29:28): So, getting some awareness in there would be your strategy?
FM (0:29:31): Yes, definitely, definitely, definitely.
MS (0:29:33): Putting that forward?
FM (0:29:34): Definitely.
MS (0:29:35): Okay.
FM (0:29:35): And I think it starts with the education part of the whole thing. I think we have taken not just one step back; we’ve taken several steps back in the last three decades since I’ve done my bachelor’s. It could have gone another way, but it hasn’t.
AL (0:29:51): You were very defensive when you were describing even the idea of introducing functional programming and teaching at your current job, but you came from a bachelor’s program that you had done many years earlier, where it seemingly was totally normal that you were being taught Scheme and Standard ML. So is that just because India is more enlightened than Switzerland, or is that because something actually changed in the meantime, or because you had this industry experience in between, which made you think, “No, this is all very esoteric,” or –
FM (0:30:31): Yeah, that’s a nice question. I have to think about that a little bit. I think it’s because when you go into an interview, you want to get the job, and you try to be as cautious as possible, and you don’t want to fray a lot of feathers. And I thought that this topic in particular is a little bit of a dicey topic. There are lots of emotions involved with this. I noticed also with my colleagues. And so I didn’t want to step on anyone’s toes with these sorts of statements. And there was more of that.
I think that once I did get the job, I would have basically lobbied to do something like this because it’s something I really believe in as well. It’s not that my belief had changed. It’s the way I thought other people perceived this area. I would be in a meeting, and people would say things like, even the MIT changed from Scheme to Python or something like that, and at least they saw the light and these sorts of things. And I normally keep quiet with such things because it’s a personal thing. That’s what people are exposed to when they – I mean, maybe I have a bias in this as well. But yeah, I just thought that it doesn’t make any sense to out myself in certain situations in this way. It’s better to just silently work according to my beliefs, my personal beliefs, and let other people choose later, maybe. And so even though I thought that this would be something advantageous, to put this out so blatantly is, I think, maybe sometimes a mistake.
AL (0:32:20): But when you’re saying that we have been regressing in the past three decades and you’re saying essentially that universities have been too eager to please industry existing practices or –
FM (0:32:34): Yes, I do think so. Yeah, that is my personal opinion. I think that there’s a lot that’s possible. I mean, take a look at this. That’s also one of the topics that I have with my students. And in general, I mean, starting to learn how to program, you’re typically introduced to concepts or to ways of programming that are very – I don’t know. I would say quick and dirty, like these block-based programming languages. They’re great, but I just sometimes feel that they’re just so one-sided. We don’t have anything like that. We don’t have anything that says, “How can I teach this to, I don’t know, like a five-year-old?” We don’t have anything like that. And that sort of puts everything in this area that the standard is like this and do get out of it. It just requires extra patience and extra effort.
So, the regressing. So the topic of the question was – I have to stay focused, sorry. My opinion that we are regressing. I think the fact that the introduction to programming has changed so drastically and that people have such a large – how do you say? They tend to think that, hey, industry is using X, where X may be Java, C, C++, and therefore we have to equip our students to do this, and the way to do this is to just learn this way of thinking and the syntax as early as possible. I do think it’s flawed. I do think it’s fundamentally flawed because it shapes the way people think about problems. And I think that, of course, at the end of the day, like in my industry experience, there wasn’t really such a big deal with just programming in Java later on. If anything, it taught me a certain discipline with how to deal with stuff. I would imagine if this was the first language that I did learn, or I mean, I did learn Java maybe even before I did learn Scheme. I’ll have to think about this. Maybe not. But the first formal language, if one thinks about it, then one is already in this area of thinking, “Oh, everything is – I have to frame my thinking in terms of this paradigm.” And I think that this is a bit strange and very – yeah, it forces people to think in a very limited way, I find.
I think that it would be better to have maybe like what you propose, Mike. Keep the language maybe even out of it, just talk about programming, about problem-solving, and take it from there. A lot of industry, university courses focus around the language, which is not great, I find. Yeah, it’s like, I don’t know, thinking about having your introduction to circuits or something like that and teaching it through SPICE or something. If you focus on one particular technology, it would be – yeah. And I think this is the way we’re going, and I would like to see it change.
MS (0:35:45): So maybe we can pick up one thing that you mentioned. I see on your knowledge on your webpage. I see something about block-based in Haskell.
FM (0:35:52): Yes. Yeah.
MS (0:35:54): Can we talk about that?
FM (0:35:56): I tried to try to punch little holes into this, and this was one of my pole punching exercises. So I get students who, after my functional programming course, come up to me and say that, “Hey, we would like to do something in this area.” And then I try to think of what we could do. And one of the things that I think deserves a lot more love is to make this way of thinking more accessible to people who are maybe starting out with programming. And this is one of the attempts that were there. So my basic thesis was the following. Many people start learning, or many people want to start learning how to program using these block-based languages like Scratch, which is great. My son uses this also, and he does have a certain feel for it. And I was thinking that, what would something like this look like for a functional language? How would we use this? I mean, we just went in with this assumption or this wish, and I think we came up with some things. What was it? We had a prototype that was there, and it was quite surprising the things we came up with. I think one of them was with types and type inference, how that really helps you construct a program. I think these are the things that people typically very often do not see the importance of or see the benefit of.
Maybe this is a side note. I mean, for the longest time, functional programming, the whole functional programming community always talked about correctness, correctness, correctness. And I don’t think that correctness is – how do I put this in a nice way? I don’t think people really care about it. I have to really think about this myself because this is an area which I spent a lot of my life on. And the sad truth about our profession is that no one really cares. This is a hard pill for me to swallow. Of course, there are people who care. And if your life depends on it, lots of money depends on it. But most often, let’s be honest with ourselves. People don’t really care.
I had a little joke, an April’s day joke. So my first lab was called the Correctness Lab at the university, and I got very few clients, zero clients. Let’s be realistic here. No one really came to me because of this name. And then one day I just made a joke, and I just changed it in German. It was Hauptsache Schnell Und Billig Lab, with the aim of getting – so the translation, I don’t know. You guys help me. “Let’s do it cheap and as quickly as possible” lab. And somehow it was a joke, but somehow it was maybe a critique to our state of industry. So I claimed that I got more customers when I had this title than Correctness Lab.
So no one really cares about correctness. And I don’t think functional programming as such, or the systematic approach to programming, is not really about correctness. I think correctness is a story that we tell ourselves. But I think there are better stories to tell ourselves. For example, it allows me to program in a better way. Yeah, that’s a better story. Or it allows me to be more efficient, a better story, I find.
AL (0:39:13): That sounds circular, though. I mean, it’s better because it allows you to program in a better way.
FM (0:39:18): Yeah, I know. You’re right. You’re right. Thanks for pushing that. Let’s see. It’s better because it allows me to be more systematic with my thought and therefore allows me to have – I don’t know. It allows me to make systematic parts of my thinking more explicit. It allows me to program in a way that makes me understand better what my code is doing. And therefore, it allows me to be more efficient somehow. Also, the whole thing of higher-order functions, everything allows me to be more efficient in some way.
I think the industry and what people – I would think that, what really drives people to program in this way? It’s that they feel that they’re more efficient. They feel that their mental strengths are being taken better. It’s more fun somehow. And I’m struggling as to what the correct story should be. I think definitely this correctness thing is not the correct story we should be telling ourselves, but more efficient.
I actually really liked one argument that Conal Elliott made a long time ago about this thing that people want performance. People will die for performance for some reason. They really say that performance, performance, performance. And I remember something, a discussion I had with one of the people in the Rust community. Someone was asking. I think it was Niko Matsakis. He’s the person in charge of this pilot for Rust. We did our PhD together at ETH, and we had the same logic colloquium. And I remember at some point, he was – maybe I’d be mistaken there later or sometime. He mentioned about linear logic and these sorts of things, and I was thinking that, “Hey, I’m having such a problem convincing people just to use normal logic for these things. Best of luck.” But it seems like the Rust people, complexity is not a problem as long as performance is there. And so performance is something that people would really do a lot for, for some reason. Correctness is not.
So I’m thinking that maybe a better story would be that, hey – what Conal Elliot mentioned some time ago was that, “Hey, what’s the actual limit of performance that I have or limit of optimization that I have?” The limit of optimization is how well do I understand the program, because the moment I don’t understand the program or understand what I’m doing, that’s the point where I stop optimizing. And so he mentioned that this way of really thinking about what my program should do allows me to really aggressively optimize my program, which other things just shaving a few bits off here and there, shaving a few cycles. This is only going to help you until a certain point. The real point is that, how well do you understand your program? How well do you understand programming? And I think our science—functional programming, formal methods, all this PL stuff—that’s where we should be putting our emphasis on.
Okay. I’ve wandered off again. Sorry.
AL (0:42:35): No, no, not at all.
MS (0:42:36): I mean, I agree about the correctness. In the developer community, a lot of people that I talk to, for them, correctness has negative connotations because they think those math people are obsessed with correctness, but they are used to working in domains where it’s not clear what correctness even means because specifications do not exist. What you often hear is the domain is messy, and there’s no single truth to things, and so on. And it’s certainly important to be able to make progress in environments like that, regardless of the fact that you don’t have a specification that would even allow you to talk about it.
FM (0:43:12): Yes, yes, that’s a very good point.
MS (0:43:14): And to be fair, in at least some of the communities that maybe Rust is big in, or where it should be big, in the embedded community, you have to see performance and correctness as both being sort of twin things that you need. So it’s really nice if your airbag opens correctly.
FM (0:43:32): Yes.
MS (0:43:33): But if it opens too late, then you run into problems. So maybe one way to look at this is that, in software architecture, we’re used to look at the whole spectrum of qualities. And I think we tend to focus on correctness, which is like one subpoint of a lot of things that are along that. But I think in functional programming, we actually have a lot to say about a lot of things that are on that spectrum, but we don’t because we’re not at home in that terminology in that community.
FM (0:44:00): Yes, you’re right. You’re right. At home in this terminology, that’s a good way to put it. Yes.
AL (0:44:05): Are we perhaps also just not using correctness in the right way? So I think a lot of time when functional programmers say it allows for writing correct programs, but they perhaps really mean – I mean, I haven’t really thought this through, basically coming from my own experience, is that it’s actually relatively easy to get something up and running relatively quickly, even from a partial specification. You just write something down, and actually – I mean, it actually is perhaps even good for the quick and dirty in a certain way. You can conjure up relatively powerful things with a few lines of code. And for that, you don’t need absolute correctness, but you need something like correct enough to be a viable prototype. I mean, perhaps that’s a thing that functional programming somehow allows or is actually good at, but we are doing ourselves a disservice of labeling it under correctness when that has these negative connotations that Mike is talking about.
FM (0:45:12): Yes.
MS (0:45:12): Yeah. And we’re too obsessive about it. And so there’s still parts of at least a German computer science community that still sound traumatized by the ’80s when the Dijkstra generation swept through computer science and said, “Well, everything that you do that is not verified is worthless.” I’m exaggerating a little bit.
FM (0:45:34): Yeah.
MS (0:45:35): So, that’s definitely a thing with some of the generation that I talked to. I remember an incident where – this was maybe a couple of years ago at a Commercial Users of Functional Programming workshop when I think Ryan Trinkle went up and he said, “Well, Haskell enables me to write really terrible programs because I can write a function that haMS2 parameters and the types will help me sort it out in a quick and dirty way.” And I remember Philip Wadler was like, “Oh, no, functional programming enables me to do bad things. We absolutely should stay away from that.” And I think Ryan was right and Phil was wrong. We should go all in on that.
FM (0:46:17): Yeah, that’s an interesting point. I think somehow we’ve snuck onto this correctness bandwagon maybe for the wrong reasons, but I think, how do we frame this in a nice way? I think maybe what we mean by correctness, maybe we should reframe this as to, “I understand better what the program does.”
AL (0:46:38): Yeah. I mean, it’s often that if I see what people are doing day to day in C or C++, then I’m terrified. I mean, if I had to do this, I could not sleep anymore. And I’m actually deeply impressed that they can. I guess it’s going back to safety belts. I mean, it’s like less about something has to be absolutely correct or something has to be absolutely verified, but it’s sort of the, you’re gently protected at all times from doing extremely bad mistakes. And even if you have a momentary lapse of concentration, you’re not going to be immediately crashing everything down. I think it’s like perhaps in terms of the overall discussion, I mean, we’ve been relatively negative for a while saying, “Oh, well, the state of the industry and we’ve been regressing,” and so on and so forth. I mean, obviously, you’re trying to do something, at least on the small, like in your courses and so on, like going in the other direction. But I mean, what’s your outlook for the future? What could we do in order to turn this around, or have we already started turning this around? Is there some light at the end of the tunnel?
FM (0:48:07): Oh, wow. I don’t know. I think – light at the end of the tunnel.
AL (0:48:18): Is it all about teaching? Is it all about just turning around education? And if so, then what is the message that we should be telling educators everywhere? What should they be doing differently, or is it just waiting until a new generation has arrived in the right places? Which has already been educated, and we just have to be patient. Or is there more?
FM (0:48:41): Yeah. This is a tricky question because it goes into people’s beliefs. And I think there are a number of things. I do believe that education does play a very big role, that if people are not exposed to these ideas, it’s just going to get lost. I was very fortunate to be in the, I say, right place, but people could say the wrong place—the right place at the right time at several places. I was fortunate enough to meet many people who are very inspiring in this area. So my mental beliefs are like this. But I do believe that education plays a big role.
The other thing I do believe is that the industry as such is a bit in a stage where it is very money-driven. It’s very fast-paced, and there’s a lot of – I just think when things start cooling down a little bit. Of course, it’s nice to have money, and I love money as well. But if our industry cools down a little bit, then people have a bit more patience and think a little bit more long-term, and I think things will start changing. I think people will think that, hey, it’s not anymore about the stock price or something like that. Everything’s cooled down now. Let’s make sure that we have a good life process for our software, and what would then be the right way to do it? I mean, at the moment it’s really like, hey, next quarter is coming. I mean, it’s AI now, it was crypto yesterday, and it was something else before that. What can we do to stock up our prices? It’s a very short-lived industry at the moment. And so I’m waiting for it to cool down, honestly, and I’ve been waiting for a long time.
And I think also maybe it requires some people with authority to also speak out about this. I mean, I guess Dijkstra, of course, he does ruffle a lot of feathers, but he was not afraid to say things. And I think at the moment, many people are just a little bit, I don’t know, meek about these things, and if they’re not, they get quite rude comments about this. And so I think there are multiple issues here. And of course, the other thing is also universities and teaching institutions are very much driven by what has happened in industry. And there are places where this is good, but there are places where this is bad. And I think in this area of teaching computer science, a lot of it is also very short-sighted. Also for industry, I believe that they would stand to gain a lot more if they put their fingers out of this.
AL (0:51:39): Perhaps towards the end, we can also, I mean, look into your personal future. I mean, in terms of your job or your teaching or your research, do you have any personal goals? Do you want to, I mean, teach more Haskell courses? Do you want to do more theorem proving?
FM (0:52:01): Yeah. So at the moment, I teach two courses in this area. One is like a functional programming course for second-semester students, and another one is a course on dependent types and Agda, which is for master’s students. I’m currently not planning on doing any more than this. Of course, I have my standard software engineering courses, but I do also a bit of theorem proving also in a very – I hide it from the big vie until it’s ready to come out. But yeah, I think from the teaching point of view, at least for my university, I think this is sufficient. I mean, we don’t have to overdo it also.
And as far as my research goes, I really do think that there are points where things I believe in are underrepresented in industry and in the public sphere. And one of them is awareness about this. I mean, that’s what I try to do with ZuriHac. It’s framed as a Haskell conference, obviously, but if you look at its topics and if you look at the speakers, it’s not really just Haskell. The motive is the systematic approach to programming, which is quite universal. I mean, we have talks about dependent types, we have talks about logic, category theory, all sorts of things. And I think that that is one thing. So public awareness about this, keeping it accessible to everyone.
Another thing I do believe is to see how this can be practically used. I think that’s something that we are sort of lacking. So in areas like, I don’t know, hardware related to programming, like microprocessors, I think there’s a lot of potential there. Teaching, there’s a lot of potential there. Robotics. So Switzerland, at least where I am, there are many robotics companies. And so I try to make it a bit more public there. Sometimes I think the people in robotics, they are mechanical engineers, they’re electrical engineers. They’re used to mathematics, and they know what’s happening. And you look at how they work, it’s a part of the algebra. I mean, they’re totally fluent in this. But the moment they have to program, they have to drop down to C. And I’m thinking this must be so traumatic for them to do this if they only knew. But the technology is somehow maybe not as there yet. So, that’s one of the other things that I’m trying to do at least the next couple of semesters, trying to see how far we can reach there. So low-level applications. I think the high-level stuff is pretty much there. I mean, you can do all sorts of crazy stuff with Haskell and this way of thinking. But the low-level stuff, people are still not convinced.
AL (0:55:07): So do you think that Haskell itself is, in principle, fine as it is, and it just needs changes in education and the mindset in order to make it more successful, or are there still changes in Haskell you would like to see, or in the ecosystem?
FM (0:55:23): Well, I’m actually quite happy with the state as it is. Of course, I wouldn’t go as far as to make any recommendations. I would say I know it’s too less for that. I think it’s really great how it is, and I really liked the way it’s going. There are lots of very smart people working on it. I think it’s really great. I think what is missing, at least in the Haskell area, is the language is changing so fast. That’s a good thing. It keeps people interested. At least it keeps me interested a lot. But I think it is very intimidating for someone to start. You can, of course, do your introductory stuff. There’s Graham Hutton’s great book, which I use in my courses. And there are lots of great blogs and everything. But we do not have a nice introduction, this intermediate-level introduction. And I can tell you from myself. I mean, as someone who has been in this functional programming, theorem proving world for like, I don’t know, 30 years now, at that time, maybe about 20 years, my first few ZuriHacs were quite challenging. It was not easy to get a hold. I mean, now after about eight years, I basically can understand each talk, hopefully. Most of them at least. But at the beginning, it was not the case. So there is some amount of – and that’s the work.
What you’re doing, Andres, with your podcast and things, I think those – there’s a lot of knowledge that’s like in people’s heads. It’s not out there. And that is something that’s, I think, missing at least in Haskell and in the functional programming world that we lack currently. Good books. Yeah, good books and good educational resources is something definitely that we lack. And I really think that Haskell, at least for me, is like a proxy for this idea of programming in a systematic way. It’s not really the language that I feel is so important. Of course, I really like it, and I use it for my courses, but it’s this sort of spirit of thinking that it allows, which I’m a big fan of. So I’m really happy that this language gets used as a vehicle to develop this further. And that would be my short answer. Sorry.
AL (0:57:40): No, okay.
FM (0:57:41): Yeah.
AL (0:57:41): Shall we leave it at that? I think –
FM (0:57:44): Yeah.
AL (0:57:45): Yeah. Thank you very much, Farhad, for taking the time to talk to us.
MS (0:57:49): Yeah.
FM (0:57:49): Thank you very much, Andres. Thank you very much, Mike. It’s been a lot of fun. And yeah, I thank you for the opportunity to speak.
Narrator (0:57:58): The Haskell Interlude Podcast is a project of the Haskell Foundation. It is made possible by the generous support of our sponsors, especially the Monad-level sponsors: GitHub, Input Output, Juspay, and Meta.
