3 ms·
It depends on what you mean by "do math". Both a proof and a program are just syntactic manipulations following a particular set of rules. The exact rules diffe
by tikhonj 13y ago
It depends on what you mean by "do math". Both a proof and a program are just syntactic manipulations following a particular set of rules. The exact rules differ, but the underlying system doesn't.
Proving something in a low-level way--just following inference rules--and executing a program are basically the same things. This is abundantly clear if you formally study operational semantics, but even people who haven't still think operationally. Of course, nobody thinks purely operationally, but then again, practising mathematicians also rely on some poorly defined "intuition".
I never claimed this makes programmers mathematicians. It doesn't. Both fiddle around with formal systems, but the goals and the actual practice differ enough to make the two fairly distinct. But they're still related and we still use the same tools to analyze both: automated theorem provers, type theory, Curry-Howard...
The fact that I can bring advancements from formal logic to bear on analyzing programming languages and the fact that I can bring advancements from programming languages to analyze proofs means this is no mere "philosophical mumbo-jumbo". This includes all sorts of things you probably think completely removed from mathematics, like verifying properties of drivers or automated debugging.
Not only is it a deep relationship to think about, it's one we regularly exploit. Even if most programmers do not acknowledge it, it exists. Really, you're saying more about the state of programmers' education than anything else.
Besides, you never really made much of a point. You made a statement and a poor analogy in its support and accused me of "abuse of language", but never said anything substantial.
- nilaykumar 13y agoQuick comment: I think people are emphasizing too much the 'logic' of mathematics, over its content. Mathematics is NOT about rigorous thinking and logical patterns (unless of course you study logic). It is much freer, pattern-based, and intuitionistic than that. It just so happens that rigorous/logical argumentation is the best way to communicate mathematics. In this sense, programming is much more algorithmic, and hence I would argue, not particularly like math (the content) at all.
- pavelrub 13y agoIf the question of the poll was "My son eats carrots, what level of piano-playing does it equal to?", would you then say that eating carrots and playing the piano are fundamentally the same, because they are both reducible to physical laws and are just manifestation of different kinds of brain activity? We all get it, and we all agree - programs can be viewed as a subset of mathematics. Every CS undergrad knows this. It is conceptually misguided to view this piece of information as revealing anything deep about what programmers do, just as it is conceptually misguided to view our ability to reduce both fishing and singing to brain activity (or to reduce everything to the laws of physics) as saying anything deep about what fishermen do. It doesn't became any less misguided simply because examples exist where math can be directly applied to programming, and vice versa. It is philosophical mumbo-jumbo because you are taking two activities with clearly distinct meaning in everyday language, and instead of simply acknowledging that we can invent a new meaning for them under which they are the same, you instead convince yourself that this new invented meaning is the only fundamentally correct one (or somehow "deeper"), and that it also has the power to show that the 'everyday' meaning is wrong. But you are not showing anything about things we already know - you are simply presenting new, different ways of looking at them, that bear little relevance to the question at hand (A circle is topologically equivalent to a square. Does it mean that our 'old' preconceptions of difference between circles and squares are now wrong?). The activity of doing mathematics, as those words are used in everyday language, is different from the activity of programming, even if in some senses (perhaps in more than one) they can be viewed as the same. The activity of running is different from the activity of fishing, even though they can be reduced to similar building blocks. I do not object to the mathematical connections you present, I object to the philosophical interpretation you give to them.