# Transcript: José Valim on unit tests and layered design (x.com/josevalim/status/2108663976855052797) > Source: > Published: 2026-10-10 02:58:36+00:00 Source: [https://x.com/josevalim/status/2108663976855052797](https://x.com/josevalim/status/2108663976855052797) · auto-transcribed with Whisper, unedited **[0:00]** Hey, everyone, so there has been many discussions on unit testing lately. And I think part of the discussion is that we likely understand different things about what unit testing is and what it is as a practice. So I thought I would record a video of a project that I'm working on and how I am writing tasks for it, okay? So this project, I'm working on it with the help of coding agents, right? I am not writing the code, but I am reviewing the code and I'm providing design directions. And in order to understand what the project does, so it is, you can write laws about Erlang and Elixir programs and you can prove them in me. **[0:49]** So I'm going to give a little bit of context because that's going to be really helpful to understand the design of the project, okay? So imagine that like, so a RtypeSystem is coming to Elixir, right? So imagine that once we, ah, I cannot type, once we add type signatures, I want to implement some, right? And this would be like a valid type signature for some, but this would be an implementation that is type check just fine. The.typechecker would accept this, right? So the type checker proves only a small amount of properties, let's say about the code, right? It says that it returns an integer, but not which kind of integer based on the arguments. And there are many ways, like if we were building these in practice, there are many ways that we could make sure that our sum implementation is better, right? **[1:44]** We could write example-based tests, right? We could just start writing, like the sum of the list, and three should be six and so on, we can write property based tests that are going to explore the search space, right? Gener bating random numbers, all of those things, they are good. All those things are going to be handful. But the goal with this project is, well, what if I I can actually prove in the implementation that it behaves, that some laws are preserved, right? So we need to think about kind of like, what are the laws and what are the properties really that we want from from this code? So one of the laws we could write, so this start venturing into what this project does is that, well, we can verify some zero and the idea here not to do is, let me pick the read me, is we can say, well, in this case, we expect that the sum of an empty list is zero. **[2:39]** So this is the base case and this will be like very easy to verify. But another law that we want, and I'm just going to copy because it's going to be easier, is that I'm going to say, well, you know, if I have two integer lists, right? Like I want that the sum of the adding together, the sum of each individual list is going to give the same result as the concatenation of those lists, right? And that is going to tell us a little bit more about the code and is going to prove more about the code than a simple type can do, right. So, and then what we do. Is that we, now we can see here in the read me is. That we can prove. And right now we can prove them in lean. Maybe we can prove those things in other languages in the future, but we can prove them in lean. **[3:27]** And the way that this works is that there is a model, I have implemented the model of the airline runtime within lean. So we have like airline, we have the same called terms, which is how we represent lists, stuff and whatever. So we have the same thing in lean now, right? We have a small model of how we send and receive messages so we can find deadlocks and all of those things. And the way that we use these, let's see if this is going to work, is that you can just, you know, you can run them. And we are using electric built-in test runner to do most of those things. I don't know if this checkout is good. This R may not work, but I can show you the code here that, you know, you're going to write it as if it was a test just because we wanna use the existing test runner, right? **[4:15]** So we have the implementation, we and we are going to go and we are going to prove that, you know, that that law is actually true using lean. So you kind of get what it's doing, right? So let's talk a little bit about how this works. And so how we're going to design how we are going to design this project and how we are going to test it. So at the very bottom of everything, we.have.something.that translates core Erlang AST. This is like a shared representation that we have like between Elixir and Erlang and so on to I call it LeanJ, which is like a JSON representation that Lean is going to receive and build the Lean AST. **[5:04]** It doesn't have to be JSON. We could use a binary format. The translation performance is not really important. So I went with a readable format, right? So that's what it does. Eventually it's going to become Lean AST. So for this layer here, right? I have implemented it. And what I did is that I implemented it using, I made it a pure abstraction that says like, there are no side effects. It doesn't read files from disk nor anything. It just receives AST and it returns AST, right? And this is a layer then that I'm going to unit test this because for example.example, let me, let's get some tests, right? So one of the things that I want to unit test, is for example, well, let me see, hold on, just give me one second. **[6:01]** So let's get this some implementation here, okay? So we have to translate that to Lean, right? And when we translate, one of the things that we want to preserve is like, line and column annotation. Because if there's something that fails in the Lean code, I want it to be able to point back to the original Elixir code, right? That's very important. But we can measure that equivalence at the AST. But if we were, only to write like, oh, let's only write black box testing. If we only use black box testing, these kind of assertions, like are we translating the lines correctly? They H would be very, very hard because the only way I could assert that would be like, oh, I'm going to write a sum that has a bug. **[7:10]** Let's see, what is the point, like in order to test that I'm converting lines correctly, we are going through the whole pipeline that is like, oh, I'm going to build an Elixir model. I'm going to start the test unit runner, runner. I'm going to translate to Lean. I'm going to run the Lean proofs only to get a diagnostic to see if the line is correct. Like to me, that's crazy, right? So of course, I, I So, let's say a function foo, and what this function foo does is that it calls bar and it calls another module. **[8:06]** Okay? Now, when I am translating this AST to a name, I can find bar, I can find plus, but now I have have to go and find it, and this other module is written in disk. So now I have this addition layer, so we have this layer which is just AST. It only works with AST, it doesn't know how to find things in disk. So I added an additional links translator layer. and what that layer does is that it's actually now it can find files, okay? So we have a small callback that we added. Let me see if I can find it a remote. Sorry, this has been like, I just decided to do this out of nowhere. **[9:00]** I am not, I have not prepared this at all. ahh But yeah, so yeah. So here there is this callback and the idea of this callback is like, hey, do I have a remote thing? So this is the penalty injection, right? It's just a dependency injection for Elixir. It's like, it's a function call, right? So this is like, hey, if I'm doing an external call I'm going to expect something in the layer above to provide me that call. And of course I'm going to unit test this but the whole goal of the next layer, the link translation, it should be smart and understand, oh, this is where modules and AST and bytecode comes from, right? And of course I have tests for this layer, right? Which is now testing those two layers because it would be extremely silly to just test this in isolation, right? **[9:48]** So yes, now I have tests aiming at this layer and I actually have some integration tests because I have this translation layer. Now I can already have tests that for example, so here I have a a bunch of tests where I have airline code, okay? And then I check the link JSON thing that I talked about and it compares with the link in presentation of those modules, right? So this is an integration test that is testing like more of the whole stack and how translation works. It compares now airline code with generated link code and this is much better, right, and this is happening at the translation layer. And then we have another layer, which is the actual more like black box testing, which is that we have cases that defined whole loss in the test suite. **[10:42]** And this is the actual whole thing, right? Like, oh, I am defining a module, right? Where is it? Okay, this is one of them, they are more. So this is actually like doing the whole thing, simulating how the test should behave and so on. So, and that's like the X unit runner integration, right? And of course, when I test this thing, it's going to test the other things. But yeah, like this is like, I have to explicitly have the intent of designing this, right? I could just like, oh, I'm not going to have any layers whatsoever, right? I'm just going to, you know, slop some code in that meshes all the layer and everything is a black box, right? **[11:30]** But if I break some small layers apart that make sense, you know, building one on top of the other, this makes like total sense individually, right? Now I can think about how, you know, how I'm going to work on the test. So if there is a regression and of like very little regret, if it was black box, every regression, everything that goes wrong would have to go to this expensive layer, right? Everything would have to go through this layer and very quickly the test suite for this project will be taking minutes, right? And then taking hours because that's the only layer we can work with, right? But you know, like now I can say, hey, well, I have a regression. Now it's better because I can work at the links translation layer that is going to be less expensive than this. And that can test a lot of things of the different interplay between modules. **[12:21]** It can test precisely the link translation and if you are getting the right result from this link translation. So this is going to be really good. And now like very specific tests when there is a regression, when somebody reports a bug in some particular case, oh, the line is not correct, right? Oh, like the variable scoping is not great here, right? I can work on this layer. But yeah, like you have to design the things and you have to teach your agent, like, hey, how do you think about the system, right? And how you're going to place tests on it. And a lot of it is going to be trial and error, and that's why you review the code because I ask the agent to write a feature and then I see that it puts things in the wrong layers, it put tests in the wrong layers. They're like, okay, you're not supposed to do that, fix that, fix that, put that into your agents in the day, right, and hopefully the next time around, you are going, it's going to do a better job and you need to give it less feedback. **[13:20]** Anyway, this I went a little bit longer than I was hoping for, but I hope it gives a little bit more of the idea, you know, when I'm thinking about testing the different parts of my application, why I think like, on layers on top of the other, not trying to isolate the middle layer. I don't think that makes sense, right? And yeah, I hope this helps.