4 ms·

There's a tremendous amount of work that's been done on trustworthy theorem provers (see LCF, HOL, HOL Light, Milawa, ...), verified SAT solving and SMT solving

There's a tremendous amount of work that's been done on trustworthy theorem provers (see LCF, HOL, HOL Light, Milawa, ...), verified SAT solving and SMT solving, proof-producing first-order solvers, etc. All of this is cool and interesting. But from an industry perspective, there's plenty to like about plain old unverified C/C++ solvers and verification tools. They might crash sometimes, and they might occasionally have a soundness problem. But the odds that (1) your prover has a bug and (2) you will accidentally exploit that bug to "prove" something that isn't true are low. To argue by analogy: plenty of people use unverified compilers, and of course these do have bugs. Even so, when your program isn't doing what you expect, it's still almost always a bug with your own code.

pfdietz 7y ago
Some on the parts of some verified compilers are not "really" verified, in that there is no proof they always work. Rather, what is proved is that IF the compiler successfully compiles the program, THEN the result is correct. This can be easier, because it only requires that the compiler be able to provide a checkable certificate that its output is correct. Consider a register allocator that uses graph coloring. In this case, the compiler just needs to check that the coloring that is produced is really a coloring: that it uses k colors, and that no two adjacent nodes in the associated graph are assigned the same color. This checking routine must be proved correct, but that's an easier task. For a theorem prover to be verified in the same way, it just needs to produce an explicit proof, and then have a proof checker that is proved correct. The theorem prover itself, the part that produces the proof, doesn't have to be shown to always work (and indeed it won't, since it will very often time out.)

pfdietz 7y ago

Some on the parts of some verified compilers are not "really" verified, in that there is no proof they always work. Rather, what is proved is that IF the compiler successfully compiles the program, THEN the result is correct. This can be easier, because it only requires that the compiler be able to provide a checkable certificate that its output is correct. Consider a register allocator that uses graph coloring. In this case, the compiler just needs to check that the coloring that is produced is really a coloring: that it uses k colors, and that no two adjacent nodes in the associated graph are assigned the same color. This checking routine must be proved correct, but that's an easier task. For a theorem prover to be verified in the same way, it just needs to produce an explicit proof, and then have a proof checker that is proved correct. The theorem prover itself, the part that produces the proof, doesn't have to be shown to always work (and indeed it won't, since it will very often time out.)