I disagree and I think you are interpreting "applied mathematics", "physics", and "computer science" overly literally - rather than labels for fields of study.
The point in the article is that programming is no longer just Applied Mathematics, it's also very much a discipline of Engineering as well. Anyone who studies these fields should understand the difference.
You are right, that these terms can apply to deep realms of human thought - but I think they are less useful terms under that definition.
If subject X is fundamentally about underlying subject Y, then reasoning using the tools of subject Y might help you to have powerful (fundamental) insights into subject X.
I take your point, nonetheless.
Programming is like mathematics, except all proofs are omitted.
By Curry-Howard, the program is the proof, albeit usually not of an interesting proposition.
Bottom is a member of every type, so all Haskell programs correspond to proofs of trivial propositions. Or that is my understanding anyway.
And something similar should be true for common imperative languages.
Not quite. Bottom as a member of every type means that you cannot trust my proof (x : A) without examining it and that your examination may be non-terminating. That said, it you examine a realizer and terminate then you have a genuine proof of a potentially non-trivial theorem.
The reason why most Haskell theorems are trivial is because lacking dependent types means that we cannot ask for interesting theorems. `3 :: Int` is a perfectly nice proof that "Integers exist" which is a little silly.
In a rich type system, a program is the proof of its own specification. Which is usually as interesting as the program itself.
Sure, but as of July 2015 the programming languages (e.g. Agda, Idris)
that can give full specifications of their own programms, are
experimental, not mainstream.
Re:New Paper: Theory of Programs
by black_knight on Monday July 06, 2015 @06:46PM
(#9842640)
«Which is usually as interesting as the program itself.» And ten times as hard to write. Not just saying that — I spend most of my time in Agda, and even simple things are rather difficult. But I think this will improve as we learn the right way to look at things.
Here's an interesting one:
Mathematicians think programming is mathematics. Programmers think they're simulating the mind of a mathematician!
This is as effective as saying "X is a branch of philosophy", where X is any discipline. It's probably true for every discipline, but what's the point?
Also every X is a branch of physics, because we live in a physical universe and everything is inside it (so even pure mathematics is a branch of physics).
And finally X is a branch of computer science because computation and information processing sometimes appears to be more fundamental than everything else. E.g., physics cannot answer the question, "are we living in a matrix-like simulation?" but if we really are, the whole physical universe is mere computation happening in some higher dimension.
I like to think of Mathematics, Computer science, Physics, and Philosophy to be deep and insightful realms of human thought, and they have many connections but also many unique attributes.