4 ms·
> Programming, wrote Dijkstra many years ago, is a branch of applied mathematics. This is as effective as saying "X is a branch of philosophy", where X is any
by fizixer 11y ago
> Programming, wrote Dijkstra many years ago, is a branch of applied mathematics.
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.
- ble 11y agoIf 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.
- arnarbi 11y agoI 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.
- amelius 11y agoProgramming is like mathematics, except all proofs are omitted.
- mafribe 11y agoBy Curry-Howard, the program is the proof, albeit usually not of an interesting proposition.
- groar 11y agoIn a rich type system, a program is the proof of its own specification. Which is usually as interesting as the program itself.
- mafribe 11y agoSure, 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.
- black_knight 11y ago«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.
- im3w1l 11y agoBottom 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.
- tel 11y agoNot 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.
- fizixer 11y agoHere's an interesting one: Mathematicians think programming is mathematics. Programmers think they're simulating the mind of a mathematician!
- Retra 11y agoA program is a proof of the result (theorem) computed from the inputs (axioms) supplied.