For purposes that would become clear in a future post, I needed to solve a curious problem in the Zig build system. Prior to that, I knew very little about it. I expected the problem to be easy to solve, and it actually is, but I discovered a lot along the way.
Here’s the problem I needed to solve: I wanted to assemble a listing with nasm and embed the machine code in the Zig program to be able to manipulate it as plain bytes. What’s interesting is that I wanted to utilize the build system to automate the process and cache/rebuild as needed.
The post is basically a write-up of my findings. The final solution is in the conclusion, but the path to there was quite fun.
When you write code, you want it to have some properties. It might be as simple as “it works”, which is the least precise the functional property :) You may also want the code to be fast, memory-efficient, and failure-tolerant. There are many properties to choose from.
Whether you are conscious about it or not, when you write code, you reason about it. You do it at least to persuade yourself that the code behaves as desired.
The problem is that all the properties you usually want to hold are global. Even the simplest “it works” talks about the program as a whole. Considering that your codebase might be hundreds of thousands of lines of code and your brain is capable of holding around 7 things simultaneously1, verifying those properties might be unbearably hard.
Even if you carry out the proof once, your code is not static, and you have to redo the whole process as soon as you change a single line. Moreover, you have to write the code line by line in the first place, being guided by something…