Comment by somat
4 hours ago
The question I always have is "why would the formal verification be any more correct than the program it is verifying?", Note: not bugs in the verification engine, but the spec made for the program.
It is not a big deal, I think formal verification is a very useful tool to help one approach correctness, but let me explain myself. When a program is written it is trying to solve a problem, when it solves that problem correctly it has no bugs, and when it solves that problem incorrectly those are bugs. For complex problems it turns out to be very difficult(impossible) to solve them correctly. Why is there an assumption that the formal verification spec will be any more correct than the program itself? They are both trying to solve very complex problems.
I was trying to get a feel for this by reading through the sel4 git changes trying to figure out how many bug fixes were for the OS and how many were for the spec. No real conclusion unfortunately. because they almost always have to fix both at the same time. a bug found in the OS means you have a bad spec and a bug found in the spec means your OS probably has a bug.
From a computer science point of view, it's the same argument as why NP-complete problems are hard to solve, and easy to check.
From a practical point of view, however, it's the same argument we write unit and integration tests. We accept error rates in the program under test, the test, the test harness, the programming language, the operating system, the hardware, and the universe. The goal is reduce the error rates enough you can ship something you can get paid for and won't get sued for later before you starve to death.
Empirically, we can look at something like CompCert, which formally verified a substantial section of a C compiler.
Subsequent high volume random testing with Csmith found no bugs in the formally verified section (unlike in every other C compiler tested with Csmith).
It should be noted that the verification performed was specifically about whether the compiler would produce incorrect code; cases where it would crash or error and not produce code would not be considered errors of verification. This would enable (for example) a coloring register allocator to be adjoined with some code that checked whether the coloring was correct and abort if not.
>why would the formal verification be any more correct than the program it is verifying?
It is quite believable that it's easier to describe what a program should result in versus actually programming it to produce that result - especially in the most common settings targeted by verification, which is to say imperative, stateful programs or algortihms with a high degree of non-obvious optimisations. The simplest example is a sorting algorithm, which normally has a trivial spec but a non-trivial state at each step.
Interestingly, some specs are actually programs themselves, as has also been true for many on-paper specs which are actually reference implementations. Research using programs-as-specs is still pretty valuable, since in some domains a simpler program is actually the right and useful way to talk about a messier one.
You know, the last time someone brought up formal verification of sorting I said what the trivial spec was, and then someone else pointed out why it's actually completely wrong.
So for pedagogical purposes, can you tell us what you think the trivial spec is?
1. The output is a permutation of the input.
2. If the comparison implements a strict total order, the output is sorted according to it.
Ok, I’ll bite, why is this wrong?
For a list of items I and an operator LEQ which returns bool for any pair of items in I, SORT() returns a list S such that:
1. Every item in I is present exactly once in S
2. For each consecutive pair of items (S_i, S_j) in S, LEQ(S_i, S_j) is true.
6 replies →
> It is quite believable that it's easier to describe what a program should result in versus actually programming it to produce that result
This is obvious for the central cases of a program. It becomes less and less true when going toward the edge cases, especially for a wide array of input.
Complex specs becoming programs is IMHO the direct effect of that (defining what we want is just that burdensome, and special cases we haven't though of will still have a coherent definition in the spec), and we fall back to the base "is this spec even correct" issue the parent points out.
Huh? Sorting does not have a trivial specification. In fact, it is usually used as the first example of how easy it is to make specification errors because it seems trivial, but is actually not.
The trivial sorting spec is actually very useful, it's just not complete. While knowing that your sorting program meets the complete spec proves it works correctly, if you wrote it intending to be a sort algorithm, and you have proven it meets the trivial spec, and you have a few unit tests, that's still very good-but-not-foolproof evidence it's correct.
do you have a reference to anywhere that discusses this further? It seems pretty trivial to me
This is valid and my take is that domain modelling becomes extremely important in this context
More then theorem proving what attracts to Lean is that it's type system is insanely powerful, indexed dependant inductive and quotient types allow the realization of "making invalid states unrepresentable" to a degree no other language can, except perhaps a custom DSL built with Racket
One must remember that Lean wasn't made for math, it ended up succeeding in that vertical because it was expressive enough to represent the extensive design space mathematicians were dealing with
And I think that's equally applicable to specs and business logic
Yeah I feel like the hype around “formal methods” is really just a growing interest in expressive type systems that enable more and more program semantics to be declared in code rather than in comments. Correctness is good, but so are portability and modularity and extensibility.
Is a type like "fixed-size list of 3 integers" really more useful than a type like "list of integers" plus a constraint "size must be 3"? I feel like the latter is more flexible. Does Lean have a type for "list containing only prime powers"?
Often the spec can be simpler than the original.
The easiest way to demonstrate this is to write two implementations of an algorithm. One with no optimizations, the other with optimizations.
The formal verification can then be a proof the optimizations maintain the semantics of the simpler version and you can focus your review on the simpler version.
Formal verification doesn't have to verify the entire functionality of the program to be useful; Rust's type system is supposed to formally verify that your program has no memory safety bugs.
(It doesn't. Because formal verification is hard. See cve-rs for how to corrupt memory without unsafe. Rust has stated they do not intend to fix cve-rs.)
Verification is sometimes less conceptually difficult than solving. I'd say for most well-defined problems, verifying is simpler.
E.g. finding a general solution for a cubic polynomial is difficult. Proving that a solution is correct is conceptually trivial: substitute a solution for x, and simplify. Many mathematical problems are well-defined in this way.
In the case of a compiler (CompCert), the program is already, in part, being written according to the language spec. So that definition can be used in verifying a compiler. In a domain where there is no standard specification or required properties, then coming up with a spec is hard (probably as hard as coming up with a solution).
> The question I always have is "why would the formal verification be any more correct than the program it is verifying?", Note: not bugs in the verification engine, but the spec made for the program.
It is a nothingburger problem because one is going to have that problem as well even when not employing formal methods. Except without FM the spec will be in natural language and therefore it will be impossible to mechanically verify the end product with it. And since natural language specs are highly liable to be ambiguous or contain unintended holes, LLMs won't save us either.