Compositional reasoning and a car
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…
read more