Open tedinski opened 2 years ago
Possibly this should be written less as patterns and more as "writing specifications"
A reasonable progression might start with:
assert
or debug_assert
sort
" tutorial specificallyThen we should mine the property testing literature for more suggestions about how to write specifications, as property tests are often interesting kinds of specifications. Including things like
We should document common patterns for proof harnesses, along with explanations/justifications for why they're common or interesting to know about.
For example:
No assumptions or assertions
It might be surprising to someone used to writing test harnesses to see a harness with no assertions, but remember that we're checking for panic-freedom by default. (Kind of like how a unit test would ensure an exception isn't thrown by default in Java.) Most functions require some assumptions to write interesting proof harnesses, but many do not. For example,
function_under_test
might return aResult
, and we may wish to prove that it's handling all possible error cases by returning an errorResult
rather than by panicking.Ideas for more welcome