I often use this when iteratively developing application source and tests - in order to validate that tests are testing what I expect, I tweak the relevant app code and run test, making sure it fails how I expect.
This lets me explore the code I’m working on, and the changes I want to make, without having to do a TDD style “reset and redo after spike”.
Similarly, breaking a type intentionally will often get GHC to tell me something I need to know. This makes development so much better.
One of my dreams for a distributed system verification system is that it would automatically support mutation testing through some kind of markup: I could mark lines in the model and say “I expect that changing this line from X to Y would violate the specification” and have the model checker check that for me. That would automated the “make it work, make it break” cycle in a principled way.
An interesting property of formal methods is that they tend to only be constructive in one direction. TLA+/TLC, for example, is great when it finds a problem, giving a really nice step-by-step trace. When it doesn’t find a problem, you just get “yup, I tried all the things and none were bad”, which isn’t helpful. SAT solvers are almost the opposite. When something is sat, you get a nice example. When something is unsat, you just get “nope, couldn’t find an example”. Some solvers give proofs on unsat, but they don’t tend to be super useful (beyond checking for solver bugs).
Whenever I write tests I try to also write the negative tests as well… if I test that 7 + 3 succeeds, then I try to have a test that makes sure 7 + false does not. It’s not a surefire thing, and maintaining it sucks, but it helps.
Reminds me of https://jsomers.net/blog/gettiers. You think your function works because the test passes. It turns out that the function really is correct, but your test was passing because the test was broken. That is, if you added a bug to the function then the test still would have passed.
haha, this is so true.
Every time I write a test that passes, I have to go break it to be sure my logic is sound. Sometimes a few tests sneak through and pass incorrectly.
I often use this when iteratively developing application source and tests - in order to validate that tests are testing what I expect, I tweak the relevant app code and run test, making sure it fails how I expect.
This lets me explore the code I’m working on, and the changes I want to make, without having to do a TDD style “reset and redo after spike”.
Similarly, breaking a type intentionally will often get GHC to tell me something I need to know. This makes development so much better.
Related: https://en.wikipedia.org/wiki/Mutation_testing
One of my dreams for a distributed system verification system is that it would automatically support mutation testing through some kind of markup: I could mark lines in the model and say “I expect that changing this line from X to Y would violate the specification” and have the model checker check that for me. That would automated the “make it work, make it break” cycle in a principled way.
An interesting property of formal methods is that they tend to only be constructive in one direction. TLA+/TLC, for example, is great when it finds a problem, giving a really nice step-by-step trace. When it doesn’t find a problem, you just get “yup, I tried all the things and none were bad”, which isn’t helpful. SAT solvers are almost the opposite. When something is sat, you get a nice example. When something is unsat, you just get “nope, couldn’t find an example”. Some solvers give proofs on unsat, but they don’t tend to be super useful (beyond checking for solver bugs).
Whenever I write tests I try to also write the negative tests as well… if I test that
7 + 3succeeds, then I try to have a test that makes sure7 + falsedoes not. It’s not a surefire thing, and maintaining it sucks, but it helps.Always get your automated tools to try and prove false from your assumptions!
Reminds me of https://jsomers.net/blog/gettiers. You think your function works because the test passes. It turns out that the function really is correct, but your test was passing because the test was broken. That is, if you added a bug to the function then the test still would have passed.
Previous discussions: