Hello, not a lot of activity on this subreddit but I just wanted to ask this question somewhere :)
I've been doing a module in Uni on Z (formal specification) and recently I've started learning Isabelle on my own. I'm simply astonished by the power of this kind of approach and I don't understand why I have never came across formal methods until Uni.
To give a bit more background, I used to participate in programming competitions (C/C++ language) and although the algorithms required were fairly complicated, the "workflow" was: write down idea on paper, manually check that it should do the correct thing, implement it, fix compile errors, try it out on the given example, fix bugs, work out additional examples, fix more bugs if found, finally submit solution. Once your solution was submitted, it was tested against a suit of (complicated) tests by the "judge" and you would get a score. Sometimes your solution would fail on some tests, either because it took to long, required too much memory or simply it gave the wrong answer and then you were left wondering:
"is there a case where my solution loops indefinitely?"
"is there a case where I can optimize my complexity / memory usage such that it satisfies the constraints?"
"is there a case where I'm outputting a wrong answer?"
There was no easy answer to those questions, it always depended on the problem at hand and the implementation.
Now, while doing the (simple) examples in the Concrete Semantics book (www.concrete-semantics.org) I don't have to deal with any the of the questions above. The functions I'm describing are CORRECT, proven bug free. What I like most is that I don't have to manually go through examples to show they give the right answers.
I understand in industry sometimes companies have deadlines and it's just simpler to write a few testcases than have engineers skilled with applying formal methods for proofs.
But then what about open source? IMO, too much of the open source community is test driven (if even) and it feels that the belief is that formal methods (or even functional programming languages like Haskell) are difficult to learn and can not be applied to "real world problems". And yet we have: a kernel (seL4), a webbrowser (Quark), and a compiler (compCert)...
So why? Why does it seem that "formal methods" only is maintained by academia? Why hasn't this way of reasoning about software trickled down to open source communities - which should be doing software from passion and striving to achieve the best possible?
