[mbo]

Given some system under test (SUT) with inputs (T, G...) and expected outputs derived from the inputs T', G' etc., a property based testing framework attempts to exercise the entire domain of values assignable to T, G, etc. against the SUT.

The generators of T, typically called an Arbitrary<T> can be constrained, e.g Arbitrary<number> could generate any float or just non-negative integers. Ideally we would define an Arbitrary<float64> or Arbitrary<u64>.

A sufficiently expressive type system makes it easier to narrow the gap between what is generated and what is assignable to type T, making it clearer what the valid input domain to the SUT is.

[sjdv1982]

I am sorry, I am not a real computer scientist and I find it difficult to find the right term. With "sufficiently expressive", I mean things like dependent types and refinement types, that can express the constraint on a unit vector.

It seems to me that this is more or less the same thing, but Monte Carlo. Like MCMC vs symbolic Bayesian inference.