4 ms·

> It provides infinitely more assurance than any amount of unit/integration testing I would say it's complementary. There are sources of error that you don't c

> It provides infinitely more assurance than any amount of unit/integration testing I would say it's complementary. There are sources of error that you don't capture in the formal model so you can't skip the test. The question is whether it's worth spending this verification effort for such an application. How much more confidence do you get, how much did you spend for it, and did you really need it? > if the spec is not correct, then testing won't help either I think that you can detect bugs in your spec when testing.

johncolanduoni 9y ago
> I think that you can detect bugs in your spec when testing. It's worth noting that when you construct and prove hypotheses in mathematics you will almost always go through an initial phase of spot testing good examples/counter-examples before you attempt a proof. So these methods are still very complementary even when you turn the abstractness up to 11.
WarDaft 9y ago
Actually that's not true. Now that we have Phantheck, all QuickCheck tests (which are a very pleasant superclass of unit tests) can just be lifted to the type level with TH magic. This makes them dramatically more useful. This is because you cannot traditionally write a function that requires that its arguments pass some test, but you can write a function that requires they have a certain type. But now you can require arbitrary QuickCheck-able properties via types. Note that you can still capture any property you want via non-metaprogramming types (though you may require a trusted kernel to keep things performant) but that can be trickier to work with than a test for people who are much more accustomed to tests than types. Also note that writing a function that should work, but won't typecheck can also reveal a flaw in the model (or in what you thought the model should be, or in what kind of operations you thought should work)

johncolanduoni 9y ago

> I think that you can detect bugs in your spec when testing. It's worth noting that when you construct and prove hypotheses in mathematics you will almost always go through an initial phase of spot testing good examples/counter-examples before you attempt a proof. So these methods are still very complementary even when you turn the abstractness up to 11.

WarDaft 9y ago

Actually that's not true. Now that we have Phantheck, all QuickCheck tests (which are a very pleasant superclass of unit tests) can just be lifted to the type level with TH magic. This makes them dramatically more useful. This is because you cannot traditionally write a function that requires that its arguments pass some test, but you can write a function that requires they have a certain type. But now you can require arbitrary QuickCheck-able properties via types. Note that you can still capture any property you want via non-metaprogramming types (though you may require a trusted kernel to keep things performant) but that can be trickier to work with than a test for people who are much more accustomed to tests than types. Also note that writing a function that should work, but won't typecheck can also reveal a flaw in the model (or in what you thought the model should be, or in what kind of operations you thought should work)