To: rocksolid.programming
Title: Property Based Testing

While formal verification is the most reliable you can get, there also exists
property based testing which comes very close to it and it's easier and faster
to implement.

There's a paper on how the Haskell containers library was formally verified in
Coq (a proof assistant) by converting the Haskell code to Coq using hs-to-coq.
They verified that the containers library had _zero_ bugs in it and it is
likely due to them using property based tests for the library. I guess it being
written in Haskell also has a huge part in it being bug free.

paper: https://dl.acm.org/citation.cfm?id=3236784
verified containers package:
https://hackage.haskell.org/package/containers-verified
talk for the paper: https://invidio.us/watch?v=9QL97E0cNk0

In short, property based testing means that you have a function and you verify
that it has specific properties. The most popular example is a sort function.

A sort function _must_ have the following properties:
* it may not change the length of the resulting list
* the resulting list must have each element the same amount of times pre and
post sort
* sorting a list twice must equal sorting the list once
* each consecutive value in a list must be greater or equal to the previous
value (ascending)

These properties are in a way formal proofs of a sort function.

QuickCheck is such a library that makes property based testing really easy. It
randomly generates input for your functions and finds the (minimal) examples
where your function doesn't satisfy those properties. If you need more
encouragement that property based testing is awesome, then check out the
computerphile video on "Code Checking Automation" on Youtube. John Huges helped
develop the Haskell language and also created QuickCheck.

video: https://invidio.us/watch?v=AfaNEebCDos

It is also possible to use property based testing on state machines to ensure
that invalid states can not be reached.
--
Posted on RetroBBS