Program calculation texts often omit proofs related to the ordering of integers, implying that readers should be able to construct them with ease. I think that’s nonsense

These texts boast about avoiding unnecessary case analyses and about the Galois connection defining ↓ and ↑ not being widely taught, yet they fail to demonstrate how to use the ↑ and ↓ calculus. And then we wonder why more people don’t use it! There have been numerous occasions during algorithm derivation where I’ve encountered an ordering constraint over the integers that high school math hasn’t prepared me for. If these texts actually showed us how to use the tools they flaunt, maybe more people would find them useful instead of frustrating.

At least it has forced me to research the area myself and refine my program-derivation skills. But it has taken me longer than necessary, had the authors been more honest about how much work goes into writing well-motivated proofs. If they acknowledged the challenges and provided comprehensive guidance, we could all benefit from a deeper understanding and more efficient learning process.

The real benefit of calculational proofs is that they emphasize programming as a goal-oriented activity. Yet, the motivations in the texts I’ve read are poorly presented, possibly masking the authors’ own lack of skill. Properly motivated proofs would not only enhance learning but also showcase the true power of calculational proofs in achieving programming goals effectively.