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.
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.
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.
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.
So for pedagogical purposes, can you tell us what you think the trivial spec is?
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.
aka, one item in I is missing in your output.
Also, SORT(1,2,3,4) = 1,2,3,4,7
but I do take the view that ( 1, 2, 3, 4, 5, 5, 6 ) is a list of seven values (perhaps the number of dollars in the pockets of seven distinct unique people) and when sorted the output should also have seven items that correspond to the seven input items.
> Also ...
Yeah, that needs tightening up by pastel8739
L = [(5,foo), (2,bar), (2,baz),...]
SORT(L, key=first) # or however it'd be specified
> You need a way to differentiate the two 5s
As there's no unique filtering or other reduction going on here, there's a permutation chain from input to output.
SORT ( 3, 2, 5, 5 ) ->> ( 2, 3, 5, 5 ) and
SORT ( 3, 2, 5, 5 ) ->> ( 2, 3, 5, 5 )
( I'm teasing, perhaps )
Every item in I is present exactly once in S
Are we talking about Values? Then inigyou is correct.
Memory locations? Then it is trivially true, but that does not prevent me from writing 0 into every memory location.
Value + Memory location? Then it does not work for arrays since we are modifying the memory locations by moving the values between them.
The abstract notion of manipulable things in a indexable order? You need to show how that correlates to reality in a way where you can not put in a hole even larger than this one you are trying to close.
To loop back, this very discussion shows how non-trivial it really is and how much thought actually needs to be put into handling even "trivial" problems. Almost everybody who talks about how we can replace these complex implementations with simpler, understandable specifications has little to no experience with the difficulties of actually creating correct specifications. Anybody who would bring up sorting as "trivial" either has no idea what they are talking about or is so far ahead that they have weird ideas as to what constitutes as "trivial". In both cases, their opinion is highly divorced from practical reality.
That is not to say that it is not worthwhile or even that the specifications are "more complex". It is quite possible the specification is still simpler despite the difficulty, but it is also likely the complex implementation was already totally incomprehensible and a simplified specification is also incomprehensible, it is now just formally incomprehensible.
You have that /s tag, but this is actually the problem with pastel8739's spec as written.
>> 1. Every item in I is present exactly once in S
This actually does require inigyou's example to be the result of calling SORT when you cannot distinguish repeated items from each other.
SORT([1,1]) => [1,1]
pastel8739's spec also doesn't exclude the possibility of inserting new values (so long as they aren't duplicates of items in the source list).
2. If the comparison implements a strict total order, the output is sorted according to it.
However, that specification is not trivial. Almost nobody correctly articulates property 1 when first encountering the problem if they do not already know the answer or are already aware it is a trick question (and even then most software developers still fail).
Furthermore, that also sidesteps the problem of formally specifying what a permutation is. Unless you have a grab bag of already proven powerful theorems, the author is most likely also going to make a error doing that as well even if we start at a proof abstraction level comparable to normal programming.
Reality is that trivial problems admit trivially wrong specifications exceedingly easily. There is little reason to assume that much more complicated problems that are hard to even articulate will magically support obviously correct specifications that are simpler and more understandable than the code.
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
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.
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).
(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.)
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.