Isn't it more like:

    Verification: code does what the specifications say

    Validation: specifications describe something we wanted to build

where with formal verification, the specifications are lower-level, so validation is extra-important.

> A good moment to remind everyone: Verification: Code does what it says. Validation: Code does what Specifications say.

Isn't this the exact opposite of what "formal verification" means? First sentence on Wikipedia [1]: "Formal verification is the act of proving or disproving the correctness of a system with respect to a certain formal specification or property."

[1] https://en.wikipedia.org/wiki/Formal_verification

Asking a LLM, I got:

- Verification: Are we building the product right?

- Validation: Are we building the right product?

My intuition was different. To me verification is a process while validation is that the outcome of that process. As in: to validate the "+" operator, you verify that 1+2=3.

Looking at the Wikipedia article https://en.wikipedia.org/wiki/Verification_and_validation the definitions are not very clear and seem to depend on the context, tough the general idea is that of the LLM answer.

Funnily enough, the https://en.wikipedia.org/wiki/Engineering_validation_test Wikipedia article is introduced with "An engineering verification test (EVT)..."

It seems to be the kind of thing where everyone has a different idea and they are often conflated, making the distinction almost meaningless without context. You can give a precise definition for your project, but it may not apply elsewhere.

Note about using LLMs: I often like to use LLMs to settle these questions. Not because LLMs are flawless, far from it, but because they work by generalizing the content of their training dataset, they should do a pretty good job on extracting consensus. It fact, it is all they do; when a LLM tells the truth, as it is often the case, it is because the consensus is often the truth.

This needs a new category:

AI verification: AI meticulously abuses all available loopholes to deliver answer expected by operator, rather than actually responding to the problem.

Simplest example: proof that `x+1 > x` (borderline impossible)

If code doesn't do what it says, isn't that a compiler issue?

It's still great if the assertions in your code are provably correct.

At the end of the day, the program was asked for by somebody, and that person described what they wanted. Whatever the program does, it can only be as much correct as much unambiguous was the description that conceived it.

The description was most likely given in a natural language, with many assumptions about the shared objective reality.

Today, we have LLMs, which de facto (but with significant flaws) formalize the interpretation of natural language, as well as the shared objective reality we inhabit. They are becoming closer to the truth than any individual human. (Their construction is a wittgensteinian program of sorts.)

So we can take an LLM with the prompt "Respond according to the following specification:" plus the original specification/requirement, in natural language, itself, as a program A.

Then we can take the written program itself, together with the emulator of the machine it runs on, as a program B.

We can feed both of these into some theorem prover - and formally prove that program A and program B give identical outputs on identical inputs. That's most likely the best we can do, ever.

(Or we can, in theory, develop programs this way, as a solution to the following question: Which program, when run on the given platform, gives provably identical answers to program A? That's a general program synthesis problem.)