Thu Jun 21 11:54:16 EDT 2018

correctness proofs

It's all about case analysis, e.g. sums, which cause multiple code
paths.  Products are somewhat automatically handled by data

(or free?  I don't dare to use that word any more).

This ties into some itching intuition I have that while producs and
sums are essentially the same (duals), they are very different in a
practical sense when it comes down to proof and program structure.

Why is this?
Is there some insight to gain here, or is this fever dream stuff?