A procedure whose result depends only on its explicit argument values and which has no observable side effects. For terminating calls with reusable results, this makes the value condition of the memoization cache contract particularly simple.
// Target: computer-science.bigb
Recursion following the constructors of a finite inductive datatype. Correctness is naturally proved by structural induction.
// Target: computer-science.bigb
Articles by others on the same topic
Even if we cannot do everything in functional, we should at least strive to clearly extract functional substes in what we do.