CONTRIBUTING: Add "little proofs" article by Matthew Prast
It contains some pretty nice advice, summarized somewhat towards the
end:
- Look for monotonicity and immutability.
- Write code that is monotonic and uses immutable data structures.
- Keep track of your pre- and post-conditions.
- Start with pre- and post-conditions and write your code around
those. Structure your code so that the pre- and post-conditions
are easy to conceptualize and verify.
- You can prove a function maintains an invariant by proving each
unit of work does.
- You should subdivide your code into the smallest possible units
that can maintain the invariant.
- Pay attention to where component boundaries act as "firewalls" that
prevent change propagation.
- Do your best to build as many of these "firewalls" as possible,
and take advantage of them when writing new features.
- Use induction to prove things about recursive functions
incrementally instead of all at once. Assume the inductive hypothesis
is already proved, and use that to your advantage.
- Write your recursive functions incrementally. Assume the recursive
call is already implemented and write the part of the function
that builds the N+1 case from the N case. Then, separately,
implement the base case.
Change-Id: I7d50750567734ddfdfcc85b764b63af0cefa0842
Signed-off-by: Andrew Jeffery <andrew@codeconstruct.com.au>
diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index 73c74d1..e64c654 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -62,6 +62,12 @@
[aria-c-is-a-protocol]: https://faultlore.com/blah/c-isnt-a-language/
+- [To be a better programmer, write little proofs in your head - Matthew
+ Prast][matthew-prast-little-proofs]
+
+[matthew-prast-little-proofs]:
+ https://the-nerve-blog.ghost.io/to-be-a-better-programmer-write-little-proofs-in-your-head/
+
## References
- [The C programming language - C Standards Committee][c-language]