The Case for Formal Verification (2013)
permalink.gmane.org
The Case for Formal Verification (2013)
1–10 of 113 posts
Re: The Case for Formal Verification (2013)
#2Yes on all counts. I never understood why the TDD culture was happy to write down a complicated function and then only verify that on input 2 the output was 4. It always seemed backwards to me especially when you could have just as easily verified that in the REPL and called it a day. To me TDD on its own is just glorified documentation and tells me nothing about the actual properties of the software. Formal proofs and verification on the other hand is definitely something everyone should be striving towards especially for foundational components of computing, e.g. compilers, virtual machines, kernels, security/network protocols, etc.
Re: The Case for Formal Verification (2013)
#3Relevant: I attended LambdaConf yesterday at CU Boulder, and there was a _great_ intro workshop for Idris, which is in the same domain as Coq. Idris is similar to Haskell (it's actually written in Haskell), but with a dependent type system, a tactic-based theorem prover like Coq has, and a bunch of other fun features.
Re: The Case for Formal Verification (2013)
#4Can someone explain why CompCert is not more popular? A formally verified compiler seems to be much more useful than something that can produce bugs.
Re: The Case for Formal Verification (2013)
#5Can someone explain why CompCert is not more popular? A formally verified compiler seems to be much more useful than something that can produce bugs.
For one you can still write buggy software in it and for another there are some limitations that can be potential deal breakers: http://compcert.inria.fr/compcert-C.html. That links spells out some of the limitations.
Re: The Case for Formal Verification (2013)
#6Can someone explain why CompCert is not more popular? A formally verified compiler seems to be much more useful than something that can produce bugs.
It doesn't support all of C99 [1]. In real-world code, you need that, plus the GNU extensions (the clang developers put in a lot of work into making clang fully compatible with gcc, going as far as accepting the same command-line switches).
Re: The Case for Formal Verification (2013)
#7Can someone explain why CompCert is not more popular? A formally verified compiler seems to be much more useful than something that can produce bugs.
It's not free software (the license permits educational and research but commercial use). I guess selling compilers to people is a hard problem in itself. :)
Re: The Case for Formal Verification (2013)
#8Can someone explain why CompCert is not more popular? A formally verified compiler seems to be much more useful than something that can produce bugs.
Even ignoring the licensing issues and limited subset of C supported, the code quality doesn't approach that of modern optimizing compilers, and the correctness proof doesn't include things like concurrency or actual machine memory models (although forks of CompCert exist for some of these), so you're still off in the unverified world if you rely on them in your code.
Also, for the vast majority of programs the possibility of bugs in the compiler is not really that impactful in terms of total effect on reliability.
Re: The Case for Formal Verification (2013)
#9Can someone explain why CompCert is not more popular? A formally verified compiler seems to be much more useful than something that can produce bugs.
Even ignoring the licensing issues and limited subset of C supported, the code quality doesn't approach that of modern optimizing compilers, and the correctness proof doesn't include things like concurrency or actual machine memory models (although forks of CompCert exist for some of these), so you're still off in the unverified world if you rely on them in your code. Also, for the vast majority of programs the possi…
The article said something about being as good as GCC with O1, is that not enough? Pardon my ignorance, I've never touched c/c++ (python guy).
Re: The Case for Formal Verification (2013)
#10Yes on all counts. I never understood why the TDD culture was happy to write down a complicated function and then only verify that on input 2 the output was 4. It always seemed backwards to me especially when you could have just as easily verified that in the REPL and called it a day. To me TDD on its own is just glorified documentation and tells me nothing about the actual properties of the software. Formal proofs a…
One big advantage is regression testing - which is why you don't just test it in a REPL and forget about it.