This is like saying all physical engineering problems are quantum mechanics (or insert other physics theory) problems. It’s technically correct (the best kind of correct), but misleading and useless as a matter of practice.

I see what you’re trying to do with the comparison, but it’s not really the same.

In your example, the two things are separated by at a minimum one layer of emergence: your example is more like saying biology is just chemistry. In maths and programming, they are both at the same level, no emergence.

I also haven’t found what you say to be true at all— As I’ve been learning more maths and more programming, and learning more about the link between the two, I have found that the ability to see problems from more than one angle has had a dramatic impact on how clearly I think and how efficiently I solve problems. Not useless whatsoever.

I was an academic physicist for the first several years of my post-graduate school career--I, too, see much value in having multiple perspectives to a problem.

But that's quite different from your other claim. Maths and programming are not at the same level. When one writes a "hello world" program, math does not figure into the final text of the code at all. Similarly, when one writes code to implement a system interacting with multiple dependencies, one is not doing mathematics, except in the trivial sense of your original comment. That is to say, at such a remote distance that it's meaningless to describe the activity as a mathematical one.

You’re doing theorem proving in all cases where you handle errors or exceptions in non-trivial fashion. Same when you’re implementing any kind of authz. When dealing with async code or threads, you’d better be good at your invariants. This is all discrete maths. Yes I don’t differentiate continuous functions at work but let me tell you juggling multiple condition scenarios when integrating multiple inputs with multiple systems is damn close to working with logic proofs.

I completely disagree, but I don’t have the energy to argue or explain.

Your analogy is interesting to me.

I definitely see the parallel, but I'm not actually sure this is true.

A lot of the deep functional stuff I'm learning right now are more about finding connections and shortcuts between things that we used think were different.

For me, comparing functional programming to older languages is more like comparing "tally marks" or "roman numerals " to a modern "place value system".

Now back to the physics analogy. The gap between quantum physics and chemistry is both a theoretical and computation limit.

There are also seen to be very distinct layers where the lower level don't seem to correlate with higher levels.

But I can also see this might apply to the Curry-Howard correspondence.

Hmmm. I have to think about it more...

Factually accurate (to some degree), but almost completely irrelevant.

First, not all problems that can be solved with code are math problems. Take driving a serial port, for instance. There might be some aspects of it that are mathematical, but mostly it's a matter of interfacing with the chip spec.

Second, even for problems that are isomorphic to a math problem... the thing about isomorphisms is that they aren't identical. One form or the other is often easier to deal with. (That's one of the reasons we care about isomorphisms - we can turn hard problems into easier ones.)

Well, which is easier, writing programs or doing proofs? Almost always, writing programs is easier. This is why it's (almost) completely irrelevant.

Nobody wants to write code that way. So nobody cares. They're not going to care, either, no matter how forcefully you point out Curry-Howard.

Now, as you say elsewhere, you can gain insights from math that can change your code. That's true. But I suspect that most of the time, you don't actually write the code as a proof.