[chriswarbo]

Property-based tests let us state the formal properties we want, even though we can't verify them. For example, ScalaCheck lets me state the following:

    forAll (x: Int) { assert(x.abs >= 0) }

This is useful as a spec, as documentation, and as a test suite: e.g. ScalaCheck can try to disprove such properties by checking a bunch of random inputs.

Whilst such approaches don't let us prove such statements (except for exhaustively checking small input spaces, e.g. `forAll (x: Boolean, y: Boolean) ...` only needs four tests), I find it just as easy as normal unit testing, and far less effort than formal proofs (e.g. using Coq or Agda)

(FYI that property is in fact false, since it doesn't hold for -2147483648; ScalaCheck's random generators are biased towards such "problematic" values, e.g. -inf, NaN, etc., so it usually find such things)