Hacker News Reader

Comment by zeteo | Hacker News Reader

Oh yes it is. Programming is exactly equivalent to writing mathematical proofs.

http://en.wikipedia.org/wiki/Curry%E2%80%93Howard_isomorphis...

I'm having a hard time seeing how you can come to that conclusion based on the article you reference. Certainly a mathematical proof can be written in a program-style formal language, and then that type of programming becomes equivalent to those types of proofs.

However, programming in general is simply not like that, and programming in general does not, to me, seem to be anything like doing math.

And since that's a very personal statement, let me add by way of context that I have a PhD in math, I have programmed for a living, and I have written computer verified proofs.

It seems to me that most of the people who claim that "programming is math" (and there are many, but perhaps not as many as the OP is implying) have never actually done any math at an advanced level.

I'd be happier saying that programming is a lot like doing word problems, where it's essential not only to get the right answer, but also to use the the right terms, with the right grammar, and in a limited amount of space.

And it's pass/fail.

>programming in general does not, to me, seem to be anything like doing math.

Hi Colin, can you substantiate that? PhD in CS here and I've done some pretty hardcore math in my academic life.

After writing lots of proofs and lots of programs the two activities don't seem that dissimilar. They are very different "programming languages" indeed, but debugging, modularity, recursion are important for both activities. To give a more concrete example: for my thesis I've implemented at one point a geometric algorithm. Some of the computer code proved buggy so I went to the white board and simply increased the complexity of the math formulas, which allowed me to write less code. I don't see an immense difference between this and, say, combining C and Python code in the same project.

  >> programming in general does not, to me,
  >> seem to be anything like doing math.

  > Hi Colin, can you substantiate that?

It's a statement about what I feel. As I say, I have a PhD in math (Pure Math: Graph Theory and Combinatorics). I have written many, many programs (both for money and not for money, both for myself and for others.)

Coming up with proofs of things believed true but not yet proven does not feel to me to be at all, in any way, like programming.

  > After writing lots of proofs ...

What sorts of proofs? Are these proofs of theorems, or are they calculations of formulas?

  > I went to the white board and simply increased
  > the complexity of the math formulas

This feels to me like you are using "doing math" in a similar way to the way that someone "uses math" when adding up the grocery bill or dividing a restaurant check (but obviously insanely more complicated). I, too, have frequently stepped to the whiteboard to make more complex calculations, or derive more complex formulas, in order to simplify computations that must be done. That's not what I call "doing math."

As I say, programming feels more to me like solving word problems, and I suspect that most of the divide and argument around this topic is caused by a lack of precision in the definition of "doing math".

Which is ironic.

Edits have been made for clarity.

>Are these proofs of theorems, or are they calculations or formulas?

A calculation is a kind of proof, isn't it? Lots of papers contain theorems and lemmas of the form "f(x) = g(x)". I don't think proving such a formula is the same as applying some well-known algorithm (grocery / restaurant bill).

And there's the difference. I do not think a calculation is necessarily a proof, but some proofs are accomplished by calculations. Some papers may contain a proof that "f(x)=g(x)" and proceed to prove the result by calculation, but that's not the only kind of proof, and it's not the only kind of calculation.

And doing the kind of calculation that's in the intersection is not then programming. Sometimes in the act of programming you will do some math, but doing the math is enabling the programming. Doing the programming is not doing the math. It's a separate activity and a separate skill.

Of course the boundaries are blurred, but I've honestly seen people write a program to take data from a database, present it nicely on the screen, and then assert that programming is just math. I doubt you're claiming that, but I've seen it claimed, and I think it's not only wrong, but misleading, and demeaning to both subjects.

Sometimes you will use math in programming, and sometimes you will use programming in math. That doesn't mean that either is the other.

And now I'm going to be controversial.

And in case anyone else is still reading, here's a theorem:

  Theorem: A prime number can be written as the
           sum of two squares if and only if it
           is of the form 4k+1 .

Just as there are many ways to write a program to accomplish a given task, there are many proofs of this theorem. If you're a programmer, and you think that programming is just math, then you should be able to come up with a proof for that theorem.

The reason this is controversial is that many mathematicians couldn't come up with a proof quickly either. Here's another:

  Theorem: A number N is prime if and only if (N-1)!+1 is
           a multiple of N.

And finally, one from my own area:

  Given a graph G=(V,E), a proper coloring is an assignment c:V->{1..n} of
  integers to vertices such that for every edge (u,v) in E, c(u) != c(v).
  (In words, color the vertices so that the endpoints of an edge are always
  colored differently).

  The "Chromatic Function" of a graph takes the number colors and returns
  the number of proper colorings.

  Theorem: For every graph, the Chromatic Function of G is a polynomial.

People say that a good programmer can pick up a new language and/or library quite quickly and become productive in fairly short order. Most of the comments on HN about hiring practices say that you shouldn't test for knowledge of language or libraries or frameworks, but for actual ability to get things done.

If programming is math, and someone is a programmer, shouldn't they be able to prove these theorems?

========

Disclaimer: This is a stronger position than I'm actually willing to defend, but I'm interested to hear people's views.

ADDED IN EDIT: I've spent way too long on this and have things I must do. I'll return later to check for any replies. I'll also get a HN_Notify email if you do reply. Or email me directly.

Not every programmer can write any program with equal ease, can we? It depends on your knowledge of available primitives: programming languages, libraries. One who knows OpenGL will have an easier time spinning a 3D model than another who parses log files for a living. Similarly, a graph theorist like yourself will find it easier to prove theorems of form 3. than the rest of us. (At least half of th. 2 seems easier though. Suppose N divides (N-1)!+1; none of 2...(N-1) divides (N-1)!+1; so none of 2...(N-1) divides N.)

I guess the main confusing part about the Howard-Curry isomorphism is that the code / comment conventions are commonly reversed between proofs and programs. Programs show a sequence of actions, and may show machine state in the comments, e.g.

...

x = x * f; //x now contains factorial(n)

...

Proofs show state instead (i.e. the proposition that was proven so far), and may contain the operation in the comments:

...

(x + y) ^ 2 = (x + y) * (x + y)

Using the distributivity of addition:

(x + y) ^ 2 = (x + y) * x + (x + y) * y

...

In either case, you:

- start with an initial state

- choose a sequence of operations from an existing set

- end up with a desired state

If either your program or proof has bugs, there are certain initial states that will break some step in the operation sequence and cause an undesired final state.

I've not been able to study the link about Howard-Curry isomorphism, but it seems largely to be talking about writing proofs in code. That's not the point. There are people who program for a living who I expect can't do that, and I expect that because I believe there are people who program for a living who can't do math (yet).

Work has taken me away and I can't reply at length. I'm trying to find a math equivalent of FizzBuzz. I still claim programming is not math, and math is not programming. Skills in each can help the other, but aren't necessary.

Engaging in the activity of programming is not "doing math."

I will return to this topic when I can - now is not a good time.

PhD in CS here as well, and I've passed on doing a lot of hardcore math. If you're going to call what I do "math," then I feel you've stretched the definition of "math" to the point that it's meaningless.

Also, one mathematician that I've worked with would object to calling CS math because he doesn't want it infecting his beautiful discipline!

What you do is math, but not all of math.

I'm not sure what that means. Clearly no one does all of math.

Did you even read the article?

Edit: This is exactly what the author is arguing against. Yes, you're writing a proof, but that's not the point of what you're doing at all.

Of course I've read it. He says just the foundations are math. He says actual programs (e.g. those implementing networking protocols) are not math. Curry and Howard beg to differ.

They can be interpreted as math, but they aren't really. If you are using Coq or something verified it can be, but especially when you are using a dynamic language and you have no idea of the types of objects that will be passed as parameters or when you are just slapdashing bits of scripts together (like, "hmm, that failed, maybe I should just +1 to it?") it's hard to compare that to the rigorous discipline called math.

Math went on for millenia without computerized proof checking and yes, some of those proofs were buggy. The difference between a professional mathematician and a software engineer is no more than that between a C and a Prolog programmer. Anyone who has written both proofs by induction and recursive programs can easily see the correspondence, even without the Curry-Haskell proof that the correspondence exists.

Most interesting programs cannot be studied analytically.

That's a pretty strong statement. Care to provide some examples?

You are correct that it's too strong. Most interesting programs cannot be fully studied analytically. The largest piece of software that has been proved correct is less than 10,000 lines of code. (Sadly, I have no reference for that - a recent speaker here talking about software testing made this claim with a reference that I have forgotten.) But real programs very quickly get to the point that it's impractical to fully understand them analytically. We have to execute them and observe their behavior.

Sorry if I seemed offensively skeptical, it wasn't my intent. I was wondering if I was missing something obvious ...which happens more than I'd like to think about. I agree with you on the lines of code. I think SeL4 is about 9,300 and I can't come up with something much longer (I don't think CompCert can really count because it's really just a lot of separate smaller programs running in succession, and generally one probably doesn't count Coq code as part of the program being verified, but everybody's got their own opinion).

I read the article and disagree. Computer science is a discipline of applied mathematics.

Saying that computer science is not mathematics because it involves real world complications, is like saying that experimental physics isn't physics because it is not done by theorists.

No, no, no. The Curry-Howard Isomorphism applies to functional programming languages only.

And if those functional languages are Turing complete, then they are equivalent to all other Turing complete languages, and thus the C-H isomorphism would hold for all Turing complete languages.

Nope. C-H concerns the simply typed lambda calculus which is not Turing-complete. Thus C-H only applies to non-recursive functional programs (or equivalent).

A proof is a program, but a program is not always a proof (as proofs must terminate).

I concede. Thanks for the interesting tangent of reading that brought on, too!

Reply on news.ycombinator.com