Hacker Newsnew | past | comments | ask | show | jobs | submitlogin

A proof is not a program.

The Curry–Howard isomorphism[1] would beg to differ. I think programming is much closer to math than this comment gives it credit for. In some sense, programming is even stricter than math. When doing math, you just have to satisfy your instructor or your reader. When programming, your program must run on a real computer -- there's no room for hand waving or imprecise arguments.

[1] http://en.wikipedia.org/wiki/Curry–Howard_correspondence



While I admit it is true in the technical sense of Curry-Howard, it is certainly not true in the sense the OP meant: that learning program is a substitute for learning mathematics.

Let's examine the post in light of C-H. I'm not super familiar with Python, but I believe it is dynamically (that is to say, singleton) typed. This might not correspond exactly to Python, but let's assume there is an any type, product types (for forming tuples in function arguments) corresponding logically to conjunction and function types corresponding logically to implication. Any well-formed expression (e.g. 0) has any type, so any is true as a proposition. Thus, all types are inhabited and all propositions are true. By proof irrelevence, the logical content of any Python program is equal to the constant function 0. In other words, they have no proof content. Thus, I claim the students here are not doing math via programming in the techincal sense of C-H.

I stand by my original claim that they are not doing math by programming in a looser sense, either. I studied computer science, spent a dozen years working as a programmer and now I'm studying math in graduate school.

> I think programming is much closer to math than this comment gives it credit for.

I might have said something like this before I started doing serious math.

You make a mistake by thinking that programming and math are the same, except that programs get "checked" by computer. That's like claiming that video games are more physically demanding than sports because the rules are enforced perfectly.

Math is about understanding why something is true. A program that uses or applies a mathematical idea rarely (never?) contains a proof of that idea's correctness. For a mathematician, testing is insufficient evidence for truth. Proofs are universal and they generally apply to an infinite number of cases. There is a deep qualitative difference between conceptually understanding why something is true and checking a finite number of cases, or even implementing a procedure to check those cases. You can try to belittle mathematical methods by calling them hand waving or imprecise, but programmers are not even trying to do what they do.




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: