Coming Soon: Machine-Checked Proofs in Everyday Development
&gt;But automation could verify this.<p>Yes, that&#x27;s what I was arguing.<p>&gt;Except that lots of business logic errors, resource handling errors, and mathematical errors still exist in modern code at all levels. And you&#x27;re also assuming the &quot;cost&quot; is &quot;stupidly high&quot; which people in this thread are telling you is false.<p>My experience with formal proofs is it imposes a high cost. I don&#x27;t think that there are people in this thread who believe that you can impose formal proofs on a system without incurring a significant cognitive overhead (and possibly other costs too). If they exist, they are simply wrong.<p>&gt;I&#x27;m not sure why you think using a computer to write proofs about your software somehow magically excludes integration tests.<p>I&#x27;m not saying that it does. I&#x27;m saying that the kinds of bugs unveiled by formal methods are, in most applications, rare and obscure and the bugs unveiled by integration tests are, in most applications, common and important.<p>When I have limited resources (everybody has limited resources), I tend to take the approach that has the best ROI in finding bugs. For most applications, that <i>isn&#x27;t</i> formal proofs.<p>&gt;Cool, except that the module integrating these, if validated, would have caught this.<p>You still aren&#x27;t getting it. The module was built upon faulty presumptions. Peter Norvig himself said that no language, no matter how type strict, would have enforced this convention.<p>&gt;The irony here: BDD is a less formal but similar technique to writing proofs.<p>I&#x27;m sorry, but writing user stories on the back of a napkin (yes, that&#x27;s BDD too) isn&#x27;t a similar technique to formal proofs in any way, shape or form.<p>BDD is simply a means of communicating example driven specs that may or may not be turned into executable user stories.<p>Automated tests (a common side effect of BDD) are not really similar to proofs either.<p>&gt;What is the difference between checking if a program properly closes a socket or if a sorting algorithm works?<p>The likelihood of bugs in the definition are significantly higher the less abstract your code gets. To wit: maybe your presumption that the socket needs to be closed is wrong.<p>&gt;Why don&#x27;t you want to make it easier to write better modules, and make it easier to verify the integration of modules?<p>I absolutely do, that&#x27;s why I use <i>the right tool for the job</i>.