What is your product goal? Both for the customer (solving a problem) and for the company(solve a marketing need, make money)?
Can you proof that you are meeting both? Then you are validating your goals successfully.
Most of the time products are missing defined goals, so lots of people have no idea what the fuck they are developing and everyone ends up with their own idea of the product.
- Did we correctly understand and build what the customer asked for
- Did the customer actually ask for what would solve the problem they are trying to solve
The second one is very important to ask early on, and _not_ asking it can cause a lot of wasted time. When I'm in a position to comment on whether I think someone fits the requirements of a senior developer, whether or not they ask that question plays directly into it.
Etymology to the rescue. "Valid" and "value" share a root, and so do "verify" and "verity." You validate something to see if it has value, meaning it works and is fit for purpose. You verify it to check that it is true and meets its specifications. Does that help? :)
Just by reading the headlines I immediately suspected the topic of Verification vs Validation would be involved. I still cannot comprehend why it is still such a gap in many software projects I have worked in. Everyone knows about testing but barely a few understand or want to understand why Validation is equally important.
While this is a good general rule of thumb, this terminology has nothing to do with how these terms are formally defined.
Verification first and foremost concerns design and development stage, a formal definition would be something like "outputs of design and development step meet specified requirements for that step". For example, you could verify that a formal specification for a module actually implements imposed requirements. Especially in software this can get murky as you cover different phases with different tests/suites, e.g. unit, integration, e2e implicitly test different stages, yet are often part of the same testing run.
Validation first and foremost concerns the whole system/product and fitness for market availability.
For example you would verify that e.g. for a motor vehicle ABS functions correctly, airbags deploy in a crash and frame meets passenger safety requirements in a crash, and you would still not be able to sell such vehicle. You would validate the vehicle as a whole with corresponding regulatory body to get vehicle deemed fit for market.
TLDR: Verification is getting passing grade in a lab test, validation is submitting all relevant lab test protocols to get CE certified.
There's this place for formal proving that most people won't get to and think it's stupid. I was such person some time ago, but then started to work on the system that: Required 2-3 months for implementation, had no room for error, made processing mistakes cost in thousands of Euros (even silly things). Than you start to wonder "hmmm... how can I use something better than just good practices and judgement? How can I _prove_ design A works".
And usually there are tangible problems to avoid: Ensuring that money won't get lost in transaction. Making sure that legal paperwork will be delivered or returned on time. Or that CSV file costing arm and leg for a single row won't have more rows than necessary. Many of these problems are borderline paradoxical. It's known that (as with Two Generals) there are no complete solutions. Usually it's like playing a catch with reality. A game that goes "what happens if we duplicate money mid-flight?" - "which system is source of truth in case of fraud", "do we rather risk false negative or accept MIA state" etc.
Sure, it's fun to model a crossroad with streetlights and a chicken just for kicks, but the main "why?" for formal proving is having "this design is good because I've seen the proof of it" moment.
But what kind of questions are asked is just as important. I can bet asbestos met all the standards it was checked against :)
You're touching on a timeless approach which is currently not possible, given the limits of reality. You'd need to know for a fact all potential outlays in order to make sure every change your program (creation) creates is accounted for and proved against. Since you do not have perfect information, your proof, by current definition, cannot be proved to be perfect.
That's true, just as I cannot possibly measure car speed given innate measuring error which is not a defense from getting a speeding ticket.
Formal proving isn't about getting to "my model is reality" but having step above mere imagination or educated guess. That's why it's possible to model paradoxical models. Given N systems they all can fail at the same time and there's nothing that can be done to guarantee message RECV+ACK. So at some point there's invariant saying "ok, we say that 3 out of 5 systems will always work". If you break invariant all hell is loose but at that point many weird stuff might happen.
Usually when one needs to think about message passing in a way like [0] formal proving can save lives (or bottoms, depending on the context).
Formal verification is ultimately an epistemological problem, how do we know that our model of reality corresponds to reality?
People have commented that validation is different from verification, but I think validation can be done by formally specifying the environment the program runs in.
For example, the question whether user can do X in your software corresponds to a question, is there a sequence of user inputs such that the software plus operating system leads to the output X.
By including the environment (like the operating system) into the formal spec we could answer (in theory) such questions.
Even if the question is fuzzy, we can today formalize it with AI models. For example, if we ask, does paint program allow user to draw a rose? We can take a definition of a rose from a neural network that recognizes what a rose is, and formally verify the system of paint program and rose verifier given by the NN.
> We can take a definition of a rose from a neural network that recognizes what a rose is
Can we? That just shifts the problem to building such a NN.
I think it would already be pretty tricky to get a decent sized panel of humans to agree on what a "rose" is. Do rose-shaped but yellow flowers count? How about those genetically altered thornless ones? How about perfectly imitatations that are made of plastic? Images of roses? The flowers from the list at https://www.epicgardening.com/rose-lookalikes/?
And of course there's the problem of getting a NN to recognise just roses. The mythical neural network with 0% error rate is exceptionally rare and usually not very useful for real world applications. I very much doubt humanity could build a neural network that perfectly recognises roses and only roses.
> The mythical neural network with 0% error rate is exceptionally rare and usually not very useful for real world applications.
I think we differ in how we see the formal methods. IMHO they are not supposed to give you 100% guarantees, because you can always cast doubt over your assumptions. Rather, I think they're a practical tool that give you a better guarantee; so in this context, a paint program verified using NN's definition of a rose is better than one that has been verified only on couple examples of a rose.
Another way to look at it - there is Curry-Howard isomorphism which states that (idealized) execution of a computer program is the same as doing logical inference, i.e. proving a formal statement. So if you're calculating 2+2, you're effectively proving that 2+2=4.
This means all software testing is a special case of a formal method. For example, when you run the test suite of your program with a new Java runtime, you are proving a statement, on these inputs my program will give the expected output, assuming we run with the new runtime. So the new runtime becomes the assumption (about the environment program runs in).
My point is, people already use formal methods, they just don't call them that. It's natural then to ask, instead of testing on a few input examples, can we instead verify a larger set of inputs (defined intensionally not extensionally)? And that's how you come from a few examples of a rose picture (extensional definition) to a definition given by an NN (intensional definition), which encompasses too-many-to-count rose pictures.
The NN doesn't have to be perfect. So what, you verified in your paint program one can also paint some pictures of not-quite-roses. Who cares? It's better verified overall.
Now you’ve just shifted the problem to a much harder statement: proving the things the NN recognizes as a rose is actually a rose.
You cannot get rid of the enviroment, and the best thing you can do is be explicit in what you rely on. For example, formally verified operating systems often rely on hardware correctness, even though the errata sheets for modern CPUs are hundreds of pages long.
Yeah. That's why I am saying it's the epistemological problem.
In the above example, that NN recognizes rose as a rose is an assumption that it is correct as a model of the (part of the) world. On that assumption, we get a formal definition of "an image of a rose in the pixelated image", and we use that to formally prove our system allows roses to be painted.
But getting rid of that assumption is I believe epistemologically impossible; you have to assume some other correspondence with reality.
I agree with you on the hardware. I think the biggest obstacle to software formal correctness is the lack of formal models of which we can be confident describe our environment. (One obstacle is the IP laws - companies do not like to share the models of things they produce.)
Right, the problem is that one can't formally describe the environment, and any one thing has to interact with it. So formallness goes right out the window.
Formal verification is a pure logic problem. You are making a proof, and a proof is just a demonstration that you can reach a given expression given certain axioms and the rules of formal logic.
You can't just chuck a neural network into the mix because they aren't formally verified to do basically anything beyond matrix multiplication and the fact that they are universal approximators.
> how do we know that our model of reality corresponds to reality?
This is the main issue I have with formal methods in commercial settings. Most of the time, the issue is that the model reality map is far from accurate. If you have to rewrite your verification logic every time you have to update your tests, development would go very slowly
Definition by consensus doesn't always equal absolute definition, to continue your epistemological metaphor. Just because the consensus states it's a rose doesn't mean it absolutely is in the truest sense (the artist, program, and neural network consensus could all be wrong in some intrinsic way).
Many interesting statements aren't a property of the code alone. They're a property of the code when it's run in a particular environment. If you want the proof to be portable then it should only make assumptions that are true in any environment.
"The assumptions are wrong" is an unsatisfying "catch-all": compiler, hardware, environment, concurrency bugs.
Here's one that's been bugging me lately: Dekker's algorithm (mutual exclusion / critical section) won't work on modern hardware. CPUs are free to rearrange reads and writes such that they still make sense under single-threaded conditions.
It's kind of put me off learning about lockfree/lockless programming. Even if I make a machine-checked proof that my concurrent code races only in acceptable ways, I have no way of knowing which instructions will be re-ordered, invalidating the proof.
Dekker's algorithm will work on modern hardware if you make use of the appropriate memory barriers. Memory barriers are essential for lock-free algorithms, so I’m not sure why that is putting you off learning them. They are, in a way, an embodiment of the assumptions underlying the algorithms, including Decker’s.
> I wrote that the "binary search" bug happened because they proved the wrong property, but you can just as well argue that it was a broken assumption (that integers could not overflow).
No, you can't argue that (well, argue that successfully). If you are trying to prove some properties of a program X written in a certain programming language Y, you can't "just assume" that the semantics of Y are different from what they are! The integers do overflow in Java, that's explicitly stated in the Java's spec.
Readit News
verification - Are we building the software right?
validation - Are we building the right software?
makes many a thing easier to talk about at work
Verification aligns with a specification. E.g. verify if what was implemented matches what was specified.
Validation aligns with a requirement. E.g. verify if what was implemented solves the actual problem.
What is your product goal? Both for the customer (solving a problem) and for the company(solve a marketing need, make money)?
Can you proof that you are meeting both? Then you are validating your goals successfully.
Most of the time products are missing defined goals, so lots of people have no idea what the fuck they are developing and everyone ends up with their own idea of the product.
EDIT: more formally, specification is a document stating requirements
Like "Customer validation" and "Verification against the spec"
Like "sympathy" and "empathy". I finally heard a mnemonic but if I need a mnemonic maybe it's a sign that the words are just too hard to understand
- Did we correctly understand and build what the customer asked for
- Did the customer actually ask for what would solve the problem they are trying to solve
The second one is very important to ask early on, and _not_ asking it can cause a lot of wasted time. When I'm in a position to comment on whether I think someone fits the requirements of a senior developer, whether or not they ask that question plays directly into it.
Verification: formal theoretical proof
Validation: Empirical test based approach
Verification first and foremost concerns design and development stage, a formal definition would be something like "outputs of design and development step meet specified requirements for that step". For example, you could verify that a formal specification for a module actually implements imposed requirements. Especially in software this can get murky as you cover different phases with different tests/suites, e.g. unit, integration, e2e implicitly test different stages, yet are often part of the same testing run.
Validation first and foremost concerns the whole system/product and fitness for market availability.
For example you would verify that e.g. for a motor vehicle ABS functions correctly, airbags deploy in a crash and frame meets passenger safety requirements in a crash, and you would still not be able to sell such vehicle. You would validate the vehicle as a whole with corresponding regulatory body to get vehicle deemed fit for market.
TLDR: Verification is getting passing grade in a lab test, validation is submitting all relevant lab test protocols to get CE certified.
And usually there are tangible problems to avoid: Ensuring that money won't get lost in transaction. Making sure that legal paperwork will be delivered or returned on time. Or that CSV file costing arm and leg for a single row won't have more rows than necessary. Many of these problems are borderline paradoxical. It's known that (as with Two Generals) there are no complete solutions. Usually it's like playing a catch with reality. A game that goes "what happens if we duplicate money mid-flight?" - "which system is source of truth in case of fraud", "do we rather risk false negative or accept MIA state" etc.
Sure, it's fun to model a crossroad with streetlights and a chicken just for kicks, but the main "why?" for formal proving is having "this design is good because I've seen the proof of it" moment.
But what kind of questions are asked is just as important. I can bet asbestos met all the standards it was checked against :)
Formal proving isn't about getting to "my model is reality" but having step above mere imagination or educated guess. That's why it's possible to model paradoxical models. Given N systems they all can fail at the same time and there's nothing that can be done to guarantee message RECV+ACK. So at some point there's invariant saying "ok, we say that 3 out of 5 systems will always work". If you break invariant all hell is loose but at that point many weird stuff might happen.
Usually when one needs to think about message passing in a way like [0] formal proving can save lives (or bottoms, depending on the context).
[0]: https://xlii.space/eng/network-scenarios/
People have commented that validation is different from verification, but I think validation can be done by formally specifying the environment the program runs in.
For example, the question whether user can do X in your software corresponds to a question, is there a sequence of user inputs such that the software plus operating system leads to the output X.
By including the environment (like the operating system) into the formal spec we could answer (in theory) such questions.
Even if the question is fuzzy, we can today formalize it with AI models. For example, if we ask, does paint program allow user to draw a rose? We can take a definition of a rose from a neural network that recognizes what a rose is, and formally verify the system of paint program and rose verifier given by the NN.
Can we? That just shifts the problem to building such a NN.
I think it would already be pretty tricky to get a decent sized panel of humans to agree on what a "rose" is. Do rose-shaped but yellow flowers count? How about those genetically altered thornless ones? How about perfectly imitatations that are made of plastic? Images of roses? The flowers from the list at https://www.epicgardening.com/rose-lookalikes/?
And of course there's the problem of getting a NN to recognise just roses. The mythical neural network with 0% error rate is exceptionally rare and usually not very useful for real world applications. I very much doubt humanity could build a neural network that perfectly recognises roses and only roses.
I think we differ in how we see the formal methods. IMHO they are not supposed to give you 100% guarantees, because you can always cast doubt over your assumptions. Rather, I think they're a practical tool that give you a better guarantee; so in this context, a paint program verified using NN's definition of a rose is better than one that has been verified only on couple examples of a rose.
Another way to look at it - there is Curry-Howard isomorphism which states that (idealized) execution of a computer program is the same as doing logical inference, i.e. proving a formal statement. So if you're calculating 2+2, you're effectively proving that 2+2=4.
This means all software testing is a special case of a formal method. For example, when you run the test suite of your program with a new Java runtime, you are proving a statement, on these inputs my program will give the expected output, assuming we run with the new runtime. So the new runtime becomes the assumption (about the environment program runs in).
My point is, people already use formal methods, they just don't call them that. It's natural then to ask, instead of testing on a few input examples, can we instead verify a larger set of inputs (defined intensionally not extensionally)? And that's how you come from a few examples of a rose picture (extensional definition) to a definition given by an NN (intensional definition), which encompasses too-many-to-count rose pictures.
The NN doesn't have to be perfect. So what, you verified in your paint program one can also paint some pictures of not-quite-roses. Who cares? It's better verified overall.
You cannot get rid of the enviroment, and the best thing you can do is be explicit in what you rely on. For example, formally verified operating systems often rely on hardware correctness, even though the errata sheets for modern CPUs are hundreds of pages long.
In the above example, that NN recognizes rose as a rose is an assumption that it is correct as a model of the (part of the) world. On that assumption, we get a formal definition of "an image of a rose in the pixelated image", and we use that to formally prove our system allows roses to be painted.
But getting rid of that assumption is I believe epistemologically impossible; you have to assume some other correspondence with reality.
I agree with you on the hardware. I think the biggest obstacle to software formal correctness is the lack of formal models of which we can be confident describe our environment. (One obstacle is the IP laws - companies do not like to share the models of things they produce.)
You can't just chuck a neural network into the mix because they aren't formally verified to do basically anything beyond matrix multiplication and the fact that they are universal approximators.
This is the main issue I have with formal methods in commercial settings. Most of the time, the issue is that the model reality map is far from accurate. If you have to rewrite your verification logic every time you have to update your tests, development would go very slowly
There was some meta-bug with encoding which almost is like an internal joke but I don't think it's intentional. The Haskell code examples have:
several times, and that `>` entity should very likely just be a `<` in the source code.Posh example: Axiom of choice.
Here's one that's been bugging me lately: Dekker's algorithm (mutual exclusion / critical section) won't work on modern hardware. CPUs are free to rearrange reads and writes such that they still make sense under single-threaded conditions.
It's kind of put me off learning about lockfree/lockless programming. Even if I make a machine-checked proof that my concurrent code races only in acceptable ways, I have no way of knowing which instructions will be re-ordered, invalidating the proof.
No, you can't argue that (well, argue that successfully). If you are trying to prove some properties of a program X written in a certain programming language Y, you can't "just assume" that the semantics of Y are different from what they are! The integers do overflow in Java, that's explicitly stated in the Java's spec.