Re: Testing relational databases

Marshall <marshall.spight_at_gmail.com> wrote:
> Now, I would argue that what we most often want is actually
> not existential quantification but universal quantification. In fact,
> what we *really* want is existential quantification, universal
> quantification, and witnesses, and we want them all available
> both at compile time and at runtime. And we want the
> witnesses to be system generated wherever possible.
>
> What we get with unit tests is existential quantification
> with programmer generated witnesses at compile time,
> so it's actually a start in the direction of what we want.

If you've got a proof that for all X, P(X), then that gets you everything you need. Assuming that the domain is non-empty, that also guarantees that there exists an X such that P(X). I don't understand why you say that you want a "witness". What good does the witness do after you've got a proof for all X (if, again, the domain of X is nonempty) ?

> Of course, we run in to problems if we begin to claim that
> we can use existential quantification to demonstrate
> universal quantification; this is of course unsound.

It seems to me that there are really two things going on here. Tests make lousy proofs. However, there are things that are hard to prove. The absence of typographical errors in a program, for example, is not amenable to sitting down and writing out a proof. As a deeper case, heuristics are often used for solving problems for which some means of formalizing a "correct" answer is not known. Often, the best one can do is to demonstrate that the heuristic seems to give fairly good results in a lot of common cases. Testing is fine for demonstrating this, and unit testing at least contains good regression testing.

I am not a fan of the pervasive unit testing fad... but it's clearly not useless. Some testing is clearly required, if nothing else just to catch the typographical error case. A line needs to be drawn, though, somewhere between there and unit testing for the correctness of algorithms.

-- 
Chris Smith - Lead Software Developer / Technical Trainer
MindIQ Corporation