Anonymous
6/12/2025, 6:42:39 PM
No.105572867
>>105572340
>Can't you just specify properties for each function and then prove that the code for that function meets them?
That's already how it works.
But consider this, you have a function which is designed to work asynchronously. As you progress further along, you realize that your model where this function is asynchronous is actually inappropriate and it needs to become serial. This causes the proof itself to radically change, and the guarantees of the function are greatly different. Now every other function with a proof which relied on this first function to be concurrent now needs to be redesigned, and functions those functions rely on, and so on. On top of any actual code that needs to be changed. In a codebase with a couple hundred thousand functions, you don't even need to change a core assumption for this to explode into an issue.
This is just an obvious example. This kind of refactor hell is actually quite common in complex, formally verified software. That's why projects which rely on formal verification aim to have a very long conceptualization period where the whole thing is planned out from the very beginning. The more complex the project, the more you end up either leaning on very specific interfaces, or very wide proof chains. In both cases, you're getting sent to refactor hell if you have to change anything meaningful. If you're in a real-time domain where you NEED to write highly impure software out of strict performance constraints the problem increases by several orders of magnitude.
>then the properties of that data structure are obvious unless you add additional restrictions on what that list can contain.
Which is unavoidable for the overwhelming majority of software. Very rarely have I ever seen an actual usecase for a list of arbitrary strings. Those strings usually have a domain and half the reason for formal verification is ensuring they actually fit the domain. EG ensuring input is fuzzed properly before it can be passed to a database.
>Can't you just specify properties for each function and then prove that the code for that function meets them?
That's already how it works.
But consider this, you have a function which is designed to work asynchronously. As you progress further along, you realize that your model where this function is asynchronous is actually inappropriate and it needs to become serial. This causes the proof itself to radically change, and the guarantees of the function are greatly different. Now every other function with a proof which relied on this first function to be concurrent now needs to be redesigned, and functions those functions rely on, and so on. On top of any actual code that needs to be changed. In a codebase with a couple hundred thousand functions, you don't even need to change a core assumption for this to explode into an issue.
This is just an obvious example. This kind of refactor hell is actually quite common in complex, formally verified software. That's why projects which rely on formal verification aim to have a very long conceptualization period where the whole thing is planned out from the very beginning. The more complex the project, the more you end up either leaning on very specific interfaces, or very wide proof chains. In both cases, you're getting sent to refactor hell if you have to change anything meaningful. If you're in a real-time domain where you NEED to write highly impure software out of strict performance constraints the problem increases by several orders of magnitude.
>then the properties of that data structure are obvious unless you add additional restrictions on what that list can contain.
Which is unavoidable for the overwhelming majority of software. Very rarely have I ever seen an actual usecase for a list of arbitrary strings. Those strings usually have a domain and half the reason for formal verification is ensuring they actually fit the domain. EG ensuring input is fuzzed properly before it can be passed to a database.