A recent blog post compared an inscrutable closed-form formula for calculating the weekday of a date into a much more readable programming language function.
This is a good reference for the “clever, analytical” bias in math, but “programming language functions” are just as formulaic; they just lack the obfuscation of a thoroughly optimized closed-form solution: For instance, the “serial number of a day in the year” can be phrased as follows:
daynum(d, m, y) is a function on natural numbers which is defined if 1 ⇐ m ⇐ 12. We will define it by induction on m:
If m = 1, then let daynum(d, m, y) = d
Otherwise, let m’ = m − 1 and l = monthLen(m’, y). Then let daynum(d, m, y) = daynum(d + l, m’, y).
Proof: see the blogpost.
The case analysis in monthLen can be expressed as is, whereas the leapyear predicate is a matter of style: neither of Van Emden’s C translations match intuition closely, but the following is reasonably intuitive and mathematically clear:
leap(y): A year y is a leap year when it is divisible by 4 and not divisible by 100, or else when it is divisible by 400.
In sum, there is no compelling reason for using C code here, except for it being easier to run on a computer: mathematical language can be just as expressive or more so.
Code has a few other advantages, though they aren’t actually being used in this case. You can type-check it, which does for some types of math what dimensional analysis does for physics. You can also bring it into automated theorem provers and verifiers, which is much harder for prose.
This is a good reference for the “clever, analytical” bias in math, but “programming language functions” are just as formulaic; they just lack the obfuscation of a thoroughly optimized closed-form solution: For instance, the “serial number of a day in the year” can be phrased as follows:
The case analysis in monthLen can be expressed as is, whereas the leapyear predicate is a matter of style: neither of Van Emden’s C translations match intuition closely, but the following is reasonably intuitive and mathematically clear:
In sum, there is no compelling reason for using C code here, except for it being easier to run on a computer: mathematical language can be just as expressive or more so.
Code has a few other advantages, though they aren’t actually being used in this case. You can type-check it, which does for some types of math what dimensional analysis does for physics. You can also bring it into automated theorem provers and verifiers, which is much harder for prose.