<story><title>The Business Case for Formal Methods</title><url>https://www.hillelwayne.com/post/business-case-formal-methods/</url></story><parent_chain></parent_chain><comment><author>Tainnor</author><text>I&amp;#x27;ve long been intrigued by pure FP, advanced type systems and proof assistants from an academic point of view but haven&amp;#x27;t yet been convinced that the effort involved in learning such systems&amp;#x2F;methods pays off in most cases (without taking into consideration the costs you still have when you already know the methods well). I will still try to learn more about this, but without any strong conviction that this needs to be immediately useful.&lt;p&gt;By contrast, I&amp;#x27;ve only more recently started hearing more and more about model checkers such as TLA+. The case studies in this blog post serve to give a good motivation for why such systems might be useful (as well as honestly presenting drawbacks; something that advocates of e.g. PFP rarely do). I would love to use something like that one day.&lt;p&gt;As an aside, I still think it&amp;#x27;s a disgrace how irrelevant empirical research is to most aspects of today&amp;#x27;s software development. Another blog post by the author cites a paper claiming that very simple testing, especially of error conditions, would be able to prevent a huge chunk of production bugs, but things like that are rarely talked about. The whole profession is unfortunately amateurish and always obsessed with fads and trends instead of taking a more analytic and empirical approach which makes me sad.</text></comment>
<story><title>The Business Case for Formal Methods</title><url>https://www.hillelwayne.com/post/business-case-formal-methods/</url></story><parent_chain></parent_chain><comment><author>kats</author><text>Might want to show some examples in the &amp;quot;Why Not To Use Formal Methods&amp;quot; section too.&lt;p&gt;Somewhat old numbers from seL4: [1]&lt;p&gt;- 2,500 lines of C code&lt;p&gt;- 100,000 lines of proofs&lt;p&gt;- ~7.6 person-years of full time work (with a lot of involvement from PhDs)&lt;p&gt;Interactive theorem proving definitely will not scale to significantly-sized C codebases anytime soon.&lt;p&gt;[1]: &lt;a href=&quot;https:&amp;#x2F;&amp;#x2F;www.ncbi.nlm.nih.gov&amp;#x2F;pmc&amp;#x2F;articles&amp;#x2F;PMC5597727&amp;#x2F;&quot; rel=&quot;nofollow&quot;&gt;https:&amp;#x2F;&amp;#x2F;www.ncbi.nlm.nih.gov&amp;#x2F;pmc&amp;#x2F;articles&amp;#x2F;PMC5597727&amp;#x2F;&lt;/a&gt;</text></comment>