My unusual hobby
I had to take a semester on formal proofs using Coq, the same tool the article talks about.<p>Putting aside their steep learning curve, formal proof methods do not guarantee that the code you&#x27;ve written is bug free. They only guarantee that the code follows the requirements you defined given the conditions you also set on your inputs. You can think of it as a mathematical proof of your postconditions will hold given that your preconditions are true.<p>And you know what? People do make mistakes establishing those preconditions and postconditions all the time, and the tool is not going to be of any help. You&#x27;ve proven your code, but it may not do what you actually wanted it to do.<p>During a lecture I saw a tenured professor, who was a well-respected mathematician and expert in Coq, make some rather obvious mistakes while establishing those preconditions and postconditions. His proof was valid but worthless.<p>When you add that writing those proofs is actually rather time consuming, you end up with a niche product with little real-world applicability, except possibly for safety-critical environments.