| › It's important to realise that variables in mathematics and variables in programming have a lot in common, but they are not the same thing! I think the stated "differences" are actually similarities with programming languages. › In mathematics, sometimes a "variable" is a place-holder for a value one may choose arbitrarily from a collection, and which is then used in some process, That pretty much perfectly describes a function parameter: for a formal correspondence, universal quantification corresponds to dependent function types. › In fact, sometimes we find that there is no value satisfying the requirements we have placed on the variable, so in a sense it doesn't exist at all! That's what happens when your variable's type turns out to be uninhabited, like an empty enum. › It seems to me, speculating idly and with no research to back me up, that recursion has similar conceptual challenges as Mathematical Induction and Proof By Contradiction. The author used proof by contradiction as part of a proof that the well-ordering principle implies the principle of mathematical induction, but (1) that links recursion and proof by contradiction exactly as much as it links recursion and modus ponens, and (2) mathematical induction is usually taken to be the more fundamental rule anyway, so this bit doesn't make much sense to me. › In mathematics a function doesn't even need to have a rule to tell you what it is, It depends on your definition of a function. ;) Related: the author lists rules such as "A finite path from an instance back to one of the simplest", which are formalized in the concept of a well-founded relation. |