<story><title>The Case for Formal Verification (2013)</title><url>http://permalink.gmane.org/gmane.comp.encryption.general/14818</url></story><parent_chain><item><author>dkarapetyan</author><text>Suppose I tell you 3 + 2 = 5 and 2 + 3 = 5. Did you learn anything non-trivial about + from those two examples? Did you learn that x + y = y + x for all x and y or that x + (y + z) = (x + y) + z? You can sample as many points as you want and you&amp;#x27;ll still be no wiser as to how + behaves and how it interacts with * or that the implementation of + even respects any of those properties. If you&amp;#x27;re going to put in the effort to generate unit tests then why not go a bit further and formally verify the correct functionality?&lt;p&gt;All this is just a roundabout way of saying I don&amp;#x27;t write unit tests. There is no value in it when I have convinced myself each subcomponent is correct and that composition of those subcomponents preserves correctness. You can write all the unit tests in the world and if you don&amp;#x27;t verify that the composition of your components preserves the correctness properties those tests are meant to verify then you might as well not have written those tests because now you have created a false sense of security.&lt;p&gt;If you can verify the kernel pieces of your code and then the composition mechanisms then you&amp;#x27;re done. You don&amp;#x27;t need to verify the entire thing as long as the entire thing is built with the kernel pieces and verified composition mechanisms that preserve correctness.&lt;p&gt;I also suspect we are still talking about separate classes of software. For your run of the mill twitter clone if it makes the corporate overlords happy then write as many unit tests as you want because it doesn&amp;#x27;t make a difference either way. But if we&amp;#x27;re talking about actual fundamental software like OS kernels and compilers then I don&amp;#x27;t think you can have enough formal verification.</text></item><item><author>stormbrew</author><text>I find it strange to think that TDD and formal verification are at odds with each other. For it to be backwards to write dynamic tests, you seem to be suggesting that it is actually worse than doing neither. I also don&amp;#x27;t see how it can be documentation, glorified or otherwise, and not tell you anything about the properties of the software.&lt;p&gt;Really there are perhaps three practical levels of knowledge about what a piece of code does:
- It does something.
- If I give it X it gives me Y (for some finite set of X).
- It will never do Z (for some finite set of Z).&lt;p&gt;The first is the state most software is in most of the time. The second is achievable with tests and some kinds of static analysis. The last is probably only achievable with formal analysis and code that fits the constraints of that formal analysis.&lt;p&gt;But both levels are at least an improvement on nothing at all. Having functional and documenting tests does bring meaningful knowledge about some subset of what the code does, even if it isn&amp;#x27;t the be-all and end-all of code analysis.&lt;p&gt;So I don&amp;#x27;t see how you can dismiss it so easily, when to me it&amp;#x27;s just a step on that striving you mention in your final sentence. For the moment it is perhaps true that the good is the enemy of the great on this, but that will become less true as the tools get better.&lt;p&gt;After all, even this article talks about only formally verifying part of the code of a web browser. Until and unless formally verifying the entire thing becomes possible, you still probably need the Acid tests to demonstrate its capabilities and help prevent regression.</text></item><item><author>dkarapetyan</author><text>Yes on all counts. I never understood why the TDD culture was happy to write down a complicated function and then only verify that on input 2 the output was 4. It always seemed backwards to me especially when you could have just as easily verified that in the REPL and called it a day. To me TDD on its own is just glorified documentation and tells me nothing about the actual properties of the software. Formal proofs and verification on the other hand is definitely something everyone should be striving towards especially for foundational components of computing, e.g. compilers, virtual machines, kernels, security&amp;#x2F;network protocols, etc.</text></item></parent_chain><comment><author>randomdata</author><text>Your test is intended to convey to the reader that your function does addition and provide an example of how to access that function. The functional part of the test is to verify that your claim is true, rather than the stories of yore when the documentation often didn&amp;#x27;t match what the code actually did.&lt;p&gt;As a nice side effect, when you refactor your function in the future and you mistakenly turn it into multiplication, the test will give you a sanity check that you meant for it to do addition. Perhaps not a big deal in your contrived example, but is huge in the real world where functions are not quite so simple.&lt;p&gt;Testing is not for verifying a function is mathematically correct.</text></comment>
<story><title>The Case for Formal Verification (2013)</title><url>http://permalink.gmane.org/gmane.comp.encryption.general/14818</url></story><parent_chain><item><author>dkarapetyan</author><text>Suppose I tell you 3 + 2 = 5 and 2 + 3 = 5. Did you learn anything non-trivial about + from those two examples? Did you learn that x + y = y + x for all x and y or that x + (y + z) = (x + y) + z? You can sample as many points as you want and you&amp;#x27;ll still be no wiser as to how + behaves and how it interacts with * or that the implementation of + even respects any of those properties. If you&amp;#x27;re going to put in the effort to generate unit tests then why not go a bit further and formally verify the correct functionality?&lt;p&gt;All this is just a roundabout way of saying I don&amp;#x27;t write unit tests. There is no value in it when I have convinced myself each subcomponent is correct and that composition of those subcomponents preserves correctness. You can write all the unit tests in the world and if you don&amp;#x27;t verify that the composition of your components preserves the correctness properties those tests are meant to verify then you might as well not have written those tests because now you have created a false sense of security.&lt;p&gt;If you can verify the kernel pieces of your code and then the composition mechanisms then you&amp;#x27;re done. You don&amp;#x27;t need to verify the entire thing as long as the entire thing is built with the kernel pieces and verified composition mechanisms that preserve correctness.&lt;p&gt;I also suspect we are still talking about separate classes of software. For your run of the mill twitter clone if it makes the corporate overlords happy then write as many unit tests as you want because it doesn&amp;#x27;t make a difference either way. But if we&amp;#x27;re talking about actual fundamental software like OS kernels and compilers then I don&amp;#x27;t think you can have enough formal verification.</text></item><item><author>stormbrew</author><text>I find it strange to think that TDD and formal verification are at odds with each other. For it to be backwards to write dynamic tests, you seem to be suggesting that it is actually worse than doing neither. I also don&amp;#x27;t see how it can be documentation, glorified or otherwise, and not tell you anything about the properties of the software.&lt;p&gt;Really there are perhaps three practical levels of knowledge about what a piece of code does:
- It does something.
- If I give it X it gives me Y (for some finite set of X).
- It will never do Z (for some finite set of Z).&lt;p&gt;The first is the state most software is in most of the time. The second is achievable with tests and some kinds of static analysis. The last is probably only achievable with formal analysis and code that fits the constraints of that formal analysis.&lt;p&gt;But both levels are at least an improvement on nothing at all. Having functional and documenting tests does bring meaningful knowledge about some subset of what the code does, even if it isn&amp;#x27;t the be-all and end-all of code analysis.&lt;p&gt;So I don&amp;#x27;t see how you can dismiss it so easily, when to me it&amp;#x27;s just a step on that striving you mention in your final sentence. For the moment it is perhaps true that the good is the enemy of the great on this, but that will become less true as the tools get better.&lt;p&gt;After all, even this article talks about only formally verifying part of the code of a web browser. Until and unless formally verifying the entire thing becomes possible, you still probably need the Acid tests to demonstrate its capabilities and help prevent regression.</text></item><item><author>dkarapetyan</author><text>Yes on all counts. I never understood why the TDD culture was happy to write down a complicated function and then only verify that on input 2 the output was 4. It always seemed backwards to me especially when you could have just as easily verified that in the REPL and called it a day. To me TDD on its own is just glorified documentation and tells me nothing about the actual properties of the software. Formal proofs and verification on the other hand is definitely something everyone should be striving towards especially for foundational components of computing, e.g. compilers, virtual machines, kernels, security&amp;#x2F;network protocols, etc.</text></item></parent_chain><comment><author>stormbrew</author><text>&amp;gt;  If you&amp;#x27;re going to put in the effort to generate unit tests then why not go a bit further and formally verify the correct functionality?&lt;p&gt;At the moment this &amp;quot;a bit further&amp;quot; is a bit like saying if you don&amp;#x27;t like the price of milk at your corner store, why don&amp;#x27;t you go to a farm to get a quart? Sure, you might be able to do that, but it&amp;#x27;s not exactly a comparable effort.</text></comment>