<i>some tools such as Verum Dezyne and Quantum Leaps can generate 100% correct source code in C, C++, Java ...</i><p>The input into these tools, from which they generate source code, is therefore, the real program and the real source code. How do they prove that this real source code, from which they generate C,C++, or Java, is "correct"?<p>In fact, this input just constitutes a new programming language -- a DSL -- and the tool is just another compiler or scripting engine. If existing compilers are unprovable, this new compiler is for the same reasons unprovable too. In other words, they did not solve the problem.
It's all definitely worth looking into. Anyone trying to start will find Wheeler's page [1] much more helpful. I also included a book [2] on using dependent types for certified programming. There's also a few examples after of verifications with [3] being pretty cutting-edge in automation & thoroughness. I think we need people to put together a single resource where newcomers can see the various approaches, tools, and practical examples of how to use them. Further, we need to research more on which tools give you the most bug hunting benefit with the least time and expertise. There's some research done already but everything in this field is scattered.<p>Another point came up in a similar discussion: we need to focus most of our energy on raising the baseline of correctness for the average programmer. This includes things such as automated test generation, design by contract, and better type systems. The developer should be able to specify his or her intention with the code while the type system or runtime catches most of the errors. Maybe we just need a version of BASIC/Pascal with Ada-like safety built-in or similar restrictions on certain constructs. Not sure of the specifics but this is an important problem to solve.<p>[1] <a href="http://www.dwheeler.com/essays/high-assurance-floss.html" rel="nofollow">http://www.dwheeler.com/essays/high-assurance-floss.html</a><p>[2] <a href="http://adam.chlipala.net/cpdt/" rel="nofollow">http://adam.chlipala.net/cpdt/</a><p>[3] <a href="https://www.umsec.umn.edu/sites/www.umsec.umn.edu/files/hardin-icfem09-proof.pdf" rel="nofollow">https://www.umsec.umn.edu/sites/www.umsec.umn.edu/files/hard...</a><p>[4] <a href="http://se.inf.ethz.ch/people/morandi/publications/prototyping.pdf" rel="nofollow">http://se.inf.ethz.ch/people/morandi/publications/prototypin...</a><p>[5] <a href="http://compcert.inria.fr/compcert-C.html" rel="nofollow">http://compcert.inria.fr/compcert-C.html</a><p>[6] <a href="http://repository.readscheme.org/ftp/papers/vlisp/guide.pdf" rel="nofollow">http://repository.readscheme.org/ftp/papers/vlisp/guide.pdf</a><p>[7] <a href="http://research.microsoft.com/pubs/122884/pldi117-yang.pdf" rel="nofollow">http://research.microsoft.com/pubs/122884/pldi117-yang.pdf</a>
(I'm the author of the original post.) Model-checkers don’t prove that a <i>program</i> is correct, only that the logic in the program’s abstracted and simplified communications/state <i>model</i> has no inherent race conditions, deadlocks and so forth, i.e. no typical concurrency flaws. Model-checkers don’t “prove” correctness in the mathematical sense (and maybe I should have written “verifiably-correct” instead of “provably-correct”). Rather, model-checkers search for counterexamples to the hypothesis “there are no concurrency flaws in this model”, by exhaustively tracing through all possible distinct execution paths through the model. Amazon calls their models “exhaustively testable pseudo-code”. If no counterexample is found, then we can be sure the model has none of the standard concurrency flaws, and we can be sure that the communications “housekeeping” code auto-generated from the model will have none either. This is a limited yet extremely powerful and valuable aspect of correctness, the hardest kind of correctness for humans to achieve in concurrent software.<p>I believe software engineers can and should start routinely using model-checking on concurrent logic, taking advantage of the machine’s ability to race relentlessly through enormous numbers of execution paths to uncover subtle flaws in logic. Even a small change to concurrent logic can have far-reaching consequences that are very hard for humans to envision. I believe competitiveness and sound engineering practice demand use of model-checkers on concurrent logic.
Okay, so the software is now provably correct.. now what were the costs in doing so, both in additional time pre-writing definitions and other abstractions for the software itself? Also, how does one prove that said software actually meets the business needs behind said software?<p>In an academic environment, or something tied to physical devices, this approach isn't a bad one at all... These are settings where software is much more akin to an engineering discipline than it is a craft.<p>In <i>most</i> software development, which are in any number of business environments building/adapting or bridging custom software that will run in any number of environments... the additional time that this will take over current approaches will be simply unacceptable. Most people don't care if a software is provably correct.. and for that matter, most bugs aren't critical in nature, and don't lead to end of the world scenarios... since most systems don't actually touch personal medical information or financial data.<p>I think on an intellectual level that approaches like this for some systems make a lot of sense... The problem is rarely do you have well defined interfaces/algorithms for well defined problems... so, you build your system with provably correct software, then the proverbial moose's neck breaks, because you didn't know about the moose.