I think the difference here is, and I don't think this is a subject that has been thought about quite enough, is that mathematics typically describe calculation, while code describes a superset of calculation, computation.
When we spend all our time working with the more expansive set, computation, we sometimes forget that calculation is in many ways less expressive and has fewer ways to express a thing. Many of the ideas in the article seem to be about getting over things we take for granted in computation, and understanding how to operate in the more limited framework offered by calculation, and/or understanding that even if things look kind of alike (what's a good word for this concept? a homoscript?) in computation vs. calculation they can be subtly different with a range of pitfalls.
The main issue with automatic translation of mathematics into code is that mathematicians often define concepts without regard for their computability.
Here are two examples:
1. Consider the set of Turing machines that halt on a certain string. This set is logically sound, but it's impossible, in general, to create a computer program that can decide membership on the set.
2. Non-constructive "there exists" style proofs. For example, take Peano's existence theorem. This helps characterize an important class of ODEs that clearly have solutions but lends no help towards actually constructing solution(s).
Mathematicians just tend to talk about this as "constructible" instead of "computable" though. My favorite illustration of this is here: http://www.scottaaronson.com/blog/?p=103
> I think the difference here is, and I don't think this is a subject that has been thought about quite enough, is that mathematics typically describe calculation, while code describes a superset of calculation, computation.
This statement is correct, but probably not for the reason you think it is.
The set of math proofs is isomorphic to the set of programs that terminate [1].
There are useful non-terminating programs (operating systems, for example), but all of the useful CS theory lies in the common subset. Data structures can completely described in math, including mutable ones.
Comments
Okay, 94 points and still no comments, I'll bite.
I think the difference here is, and I don't think this is a subject that has been thought about quite enough, is that mathematics typically describe calculation, while code describes a superset of calculation, computation.
When we spend all our time working with the more expansive set, computation, we sometimes forget that calculation is in many ways less expressive and has fewer ways to express a thing. Many of the ideas in the article seem to be about getting over things we take for granted in computation, and understanding how to operate in the more limited framework offered by calculation, and/or understanding that even if things look kind of alike (what's a good word for this concept? a homoscript?) in computation vs. calculation they can be subtly different with a range of pitfalls.
The main issue with automatic translation of mathematics into code is that mathematicians often define concepts without regard for their computability.
Here are two examples:
1. Consider the set of Turing machines that halt on a certain string. This set is logically sound, but it's impossible, in general, to create a computer program that can decide membership on the set.
2. Non-constructive "there exists" style proofs. For example, take Peano's existence theorem. This helps characterize an important class of ODEs that clearly have solutions but lends no help towards actually constructing solution(s).
Mathematicians just tend to talk about this as "constructible" instead of "computable" though. My favorite illustration of this is here: http://www.scottaaronson.com/blog/?p=103
Interesting distinction that rings really quite true.
Interesting but recent thread on it http://news.ycombinator.com/item?id=3227620
> I think the difference here is, and I don't think this is a subject that has been thought about quite enough, is that mathematics typically describe calculation, while code describes a superset of calculation, computation.
This statement is correct, but probably not for the reason you think it is.
The set of math proofs is isomorphic to the set of programs that terminate [1].
There are useful non-terminating programs (operating systems, for example), but all of the useful CS theory lies in the common subset. Data structures can completely described in math, including mutable ones.
[1] See the Curry-Howard isomorphism.
Do you know anything about mathematics?