Comment by mentalgear
2 hours ago
A good moment to remind everyone:
Verification: Code does what it says.
Validation: Code does what Specifications say.
Specifications: Were hopefully correctly modeled to the Problem.
In IEEE terms:
> Verification: "Are we building the product right?" > Validation: "Are we building the right product?")
You can write mathematically flawless code that highly efficiently solves the wrong problem.
---
While I think formal verification is the future (essential for cybersecurity), it's not a silver bullet for the other 2 items, which are way more ambiguous. I think however they can all iterate on each other and improve the project overall, but it still depends on competent steering
If you have had experiences with good approaches for verification Validation & Specification framework, do let us know about them.
Isn't it more like:
where with formal verification, the specifications are lower-level, so validation is extra-important.
> where with formal verification, the specifications are lower-level, so validation is extra-important.
Specifications don't need to be lower-level. They also compose nicely. Ie you can figure out how to formally specify a 'this doesn't crash' requirement once, and then re-use it on all your projects.
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)
> 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
It's still great if the assertions in your code are provably correct.