How to Fix a Song (Synthesis and Repair with Types and Tests)

[Music] hi my name is m and today I'm going to tell you a little bit about my research so I do synthesis and repair with types and tests but what I'm going to tell you today is how to fix a song so my background is that I work at the intersection of programming languages and software engineering and my thesis is focused on program repair where we automatically fix issues with code uh using types and tests so why and who are we doing it for well half the time spent programming is spent debugging so the idea is if we can automate that then we can save developers time but let me tell you a little bit about what we are doing so code is a bit like lyrics so in this case uh it's Happy Birthday to You song but it's been changed a bit to make it a bit funny so when you write lyrics you have to stick to certain rules you have to make sure that the lyrics fit the tune and you have to make sure that it has it rhes so let's look at this song happy birthday to you you live in the Sue you look like a monkey and you smell like one also see that last line it it doesn't really fit right the last word doesn't rhyme and it makes the whole song Sound a bit off so this something wrong with the lyrics here even if the rest kind of all makes sense the last one makes the whole thing wrong and because we've heard so many songs before we can already tell that it's the last word that wrong so this is a process called fault localization where we try to figure out what causes something to be wrong so here we know that the last word does not rhyme with the first two words U and Sue so what is the rule here well the rule is that that last word has to have this oo sound so one way we say talk about this in computer programming is that we say that these things have types so we give it some uh idea of what shape it should be and then we use that shape to figure out what should go where so the types here is that we want these things to have a newo sound so the first one U has a new sound and the second one Su has a new sound but the third one also has a so sound so it doesn't fit the same shape so how can we fix this fix this program or fix these lyrics well what we do is that we take out the wrong word and we replace it with a hole so because we know that the this hole has a type we call it a type hole so the type of this hole here is the oo sound so we're saying that whatever we put in here should have an oo sound so this allows us to focus our program repair on this specific part and in the meantime we kind of forget about the rest of the program so now that we know what part of the program is wrong and what shape that part should have we can try coming up with some Replacements now this process is called synthesis so synthesis is when you have some specification in this case the types and then you try to come up with something that fits that specific so let's think of something okay U okay yeah that has the U Sound Works through and through okay yeah it has the u sound so it fits the shape two okay yeah sure fits the shape but do they all work so if we say you smell like one U well we're repeating the U from before so it works but it doesn't really fit what we want for a usually when we rhyme in a song we want to use different words so it's not just the shape that matters but also which words we use so to test this we use testing so we have to figure out how can we tell that we want to have a unique word here where we write a test and we say that the whole should not be you and the whole should not be Sue Okay so now we can eliminate you it doesn't match the test Suite so we can't use that word so what about through and through well it has the oo sound but if we sing it and you smell like one through and through we have to kind of sing it a bit fast so it it doesn't quite fit uh what we want from this song so how do we fix that well we just add another test we say that ho has to be one syllable we want it to be short to kind of fit the rest of the two okay so what about two well it has the right shape it has the u sound it's not U it's not Sue and it's one syllable so we match all the things that we need from the specification and so we can just put it in the hole that's what we talk about when we talk about repair we just replace the hole with the thingle that we found all right so now by replacing the ho it finally sounds good all right and that's what we do that's how we repair programs and of course it's not always this easy and my f research is focusing on the fault localization so figuring out which parts of the program is wrong uh I figure out how to make good guesses guesses with the synthesis and finally uh bring it all together into this one automatic repair program so let's think about a bit like who is it for where can we get it and when is it available well the first part the type TOS in the whole pH synthesis that got added to the Haso programming language that I usually use way back in 2018 so when the main compiler for the high school programming language you've been able to use this uh guess coming up with Replacements since 2018 uh since 2022 it has been this automatic repair program for Haso uh we called it proper and it takes in hll code and tries to do this automatic program repair now currently it only works for uh small programs but we're working on making that better so uh better fult localization uh in this case something called tracing where you kind of keep track what you were doing has been proposed uh for this GHC compiler and we're in the process of making the shaping up the proposal and making it so that it can get into the compiler itself and makes it available for everyone that's using the language now we have some more ideas about the better F localization uh but it's currently in the work so I can't really share that now U and then we're going to bring that all together uh the better Replacements the better fault localization and uh bring it all together into one big program uh and make it so that you can repair any high school program easily without putting in too much effort all right uh that's the overview of my research I hope you learned a bit about how program repair works and I hope that you come to me and ask any questions that you might have thank [Music] you this was a popular science presentation from Chalmer University of Technology in Sweden