The answer is that QuickCheck can't correctly constructively verify an existential condition without a constructive mechanism to generate the existential (i.e. the Skolem function mentioned before).
I agree but don't think it's relevant. QuickCheck can't verify a universal either.
If [elided] you can abuse [QuickCheck] but unfortunately this costs you the invariant that when quickcheck says something is wrong that something really is wrong.
And to me at least the value of QuickCheck is that it never cries wolf.
It's a great point, and I agree completely. I guess what I would like is to reuse most of the mechanisms in QuickCheck to have it say one of these two things: 1. Found an satisfying instance after 73 tries: [gives instance] 2. After 100 tries, could not find a satisfying instance. Like failure, the first tells you something definite about your program. And like passing 100 tests, the second tells you nothing. Norman