4 ms·

> Dijkstra […] then proceeds to argue how programming is just a branch of mathematics. Which it is. In a trivial sense, programming languages are formal syste

> Dijkstra […] then proceeds to argue how programming is just a branch of mathematics. Which it is. In a trivial sense, programming languages are formal systems. Even when poorly specified, the computer they run on is a formal system. In a less trivial sense, we have the Curry-Howard correspondence. In a very real sense, programming language designers have denotational and operational semantics. Fuzzy systems need not get rid of mathematics. They just switch from first order logic to probability theory (or a computationally tractable approximation). Ignorance of basic mathematics is why so many fools believe lambdas or monads are hard to understand. It feels like we're scared of abstractions. For instance, we solve linear equations every time we go to the grocery and pay cash. Yet being presented with those linear equations as such, get us running away screaming into the night. --- Programming is applied math, period. The question is, which kind of math do we want to use? Which are the more useful notations, formalizations, theorems? How does all that relate to the old math?

seanmcdirmid 13y ago
In a trivial sense, life is a formal system. Even when poorly specified, the universe we run in is a formal system. Everything is then math, period. The question is, which kind of math do we want to use to reason about life? Hey, when you figure it out, let me know.
dagw 13y ago
I disagree. Computer Science might be a branch of mathematics, but computer science is also just a part of programming. Programming also involves things like software design and engineering and human computer interaction which are not a branch of mathematics. Programming is like building a bridge. Yes lots and lots of math is involved in building a successful bridge, but claiming that bridge building is just a branch of applied mathematics is kind of missing the forest for the trees.
- loup-vaillant 13y ago
  > Programming is like building a bridge. Not quite. When you build a bridge, you'd better doing according to spec, or it will collapse. The specs better be sound according to the known (mathematical) laws of physics, or it will collapse. Lot's of theorems to use, and lots of proving your design is sound. Software is often more lenient, and as such less mathematical than bridge building. But that doesn't help my point. How would you go about proving a mathematical conjecture? You think, you talk to colleagues, you try approaches, you design tools (notations, programs that do math…). That's less formal than you might think. Heck, the proof you provide in the end is often not even machine checked! Coq users are often more rigorous than the most die hard mathematician in this respect. Just like software writing and bridge building, the process of doing math is not mathematically formalized. In that sense, there is a lot more to math than math.
  - seanmcdirmid 13y ago
    Only a bit of math goes into building a bridge, though. It's not like the construction workers are continuously solving differential equations. Even when the specification is being written, math is just a tool to deal with constraints that are not identified using math. Quite similar to programming actually.
    - loup-vaillant 13y ago
      > Even when the specification is being written, math is just a tool to deal with constraints that are not identified using math. I beg your pardon? You have to model the weather, come up with a whether distribution over the years, a probability of collapse each time you encounter such and such circumstance… The constrained are not only identified using math, they're often pinned down with math. > It's not like the construction workers are continuously solving differential equations. Sure. But when the differential equation tells them to screw that bolt here, they better screw that bolt here, or compromise the integrity of the bridge.
      - seanmcdirmid 13y ago
        Right, but how many mathematicians does it take to build a bridge? Probably just a few engineers, and the process is probably very standardize. That architect probably isn't using much math in his/her design. Software is similar: there is some math involved, but it is often abstracted away and you might not ever be exposed to it.
  - brudgers 13y ago
    Software practice is more lenient than bridge building practice, but only by virtue of being so new as to escape regulation. There's nearly four fucking millennia worth of precedent for regulating construction because people die from blunders. The lack of accountability for the consequences of programs is unlikely to remain the context for practicing development. But even 25 years ago The Morris Worm was a treated as a felony and the list of actions for which there is criminal or civil liability has only grown. At some point normal programming activities will entail the risk of such liabilities to a degree that programming entails a formal standard of care like architecture and civil engineering and orthopedic surgery. https://en.m.wikipedia.org/wiki/Code_of_Hammurabi https://en.m.wikipedia.org/wiki/Code_of_Hammurabi
stiff 13y ago
Computers are formal systems as much as an alternating electrical current is a complex number, same with programming languages, even though both programming languages and formal systems can be viewed as abstract entities. Technically speaking all that can be said is that certain programming languages can be models for certain formal systems, and there is a big difference between being a model for a formal theory and something simply being only a formal theory: http://en.wikipedia.org/wiki/Reification_%28fallacy%29 http://en.wikipedia.org/wiki/Reification_%28fallacy%29 Programming language designers of most popular programming languages have no clue about neither denotational nor operational semantics and make use of no formal theory whatsoever. Anyhow, I do not deny the importance of various kinds of mathematics for programming, in some selected places and in the sense of writing programs that do mathematics. I am saying two things: - The attempts so far to turn programming itself into a single mathematical theory have failed miserably. Can you name one really important algorithm that was discovered by doing derivations in a formal axiomatic theory of programming? There is the "Algebra of programming" theory by Bird, the "Elements of programming" by Stepanov, but nothing particularly striking seems to ever come out of it, only proofs of things we already know. - There are hundreds of aspects of programming that have nothing to do with mathematics and turned out to be of far bigger importance than finding effective means of formal correctness proofs of programs. To give one example, programmers have to work in teams with the size of problems we are dealing with today, something the formal methods people never seemed to address much, and issues with communication and coordination cause much more problems than simple logical errors in algorithms.
- loup-vaillant 13y ago
  > Programming language designers of most popular programming languages have no clue about neither denotational nor operational semantics and make use of no formal theory whatsoever. That may explain why so many of our popular languages have several glaring flaws. Java doesn't support tail calls dammit! We had to wait for scheme to finally have lexical scope! C++ is impossible to parse! > The attempts so far to turn programming itself into a single mathematical theory have failed miserably. Wait, what attempts? I've read many Haskell papers, and did not stumble upon such a thing.
userbinator 13y ago
It feels like we're scared of abstractions. For instance, we solve linear equations every time we go to the grocery and pay cash. Yet being presented with those linear equations as such, get us running away screaming into the night. Because it is far easier to see value in solving real-world problems than to think in terms of just abstractions; and at the end of the day, real-world matters. Computers were invented for solving problems in reality, and that is one thing that should always be kept in mind when programming them. Abstractions, while powerful, also have a cost, both mentally and in terms of computing resources, and the latter is definitely finite, so being scared of them is both natural and reasonable. To put it bluntly, how many programmers don't know what "Curry-Howard correspondence", "first order logic", or "denotational and operational semantics" are, and yet have written hugely useful and popular applications? I argue that there is very little math and theory that one must know to do great things with programming - arithmetic and algebra are sufficient. So I believe we may see some truly wonderful things when we stop propagating this notion that computer science is hugely abstract maths, and instead focus on its more concrete aspects. (I touch on this point here too: https://news.ycombinator.com/item?id=7672252 https://news.ycombinator.com/item?id=7672252 )

seanmcdirmid 13y ago

In a trivial sense, life is a formal system. Even when poorly specified, the universe we run in is a formal system. Everything is then math, period. The question is, which kind of math do we want to use to reason about life? Hey, when you figure it out, let me know.

dagw 13y ago

I disagree. Computer Science might be a branch of mathematics, but computer science is also just a part of programming. Programming also involves things like software design and engineering and human computer interaction which are not a branch of mathematics. Programming is like building a bridge. Yes lots and lots of math is involved in building a successful bridge, but claiming that bridge building is just a branch of applied mathematics is kind of missing the forest for the trees.

loup-vaillant 13y ago
> Programming is like building a bridge. Not quite. When you build a bridge, you'd better doing according to spec, or it will collapse. The specs better be sound according to the known (mathematical) laws of physics, or it will collapse. Lot's of theorems to use, and lots of proving your design is sound. Software is often more lenient, and as such less mathematical than bridge building. But that doesn't help my point. How would you go about proving a mathematical conjecture? You think, you talk to colleagues, you try approaches, you design tools (notations, programs that do math…). That's less formal than you might think. Heck, the proof you provide in the end is often not even machine checked! Coq users are often more rigorous than the most die hard mathematician in this respect. Just like software writing and bridge building, the process of doing math is not mathematically formalized. In that sense, there is a lot more to math than math.
- seanmcdirmid 13y ago
  Only a bit of math goes into building a bridge, though. It's not like the construction workers are continuously solving differential equations. Even when the specification is being written, math is just a tool to deal with constraints that are not identified using math. Quite similar to programming actually.
  - loup-vaillant 13y ago
    > Even when the specification is being written, math is just a tool to deal with constraints that are not identified using math. I beg your pardon? You have to model the weather, come up with a whether distribution over the years, a probability of collapse each time you encounter such and such circumstance… The constrained are not only identified using math, they're often pinned down with math. > It's not like the construction workers are continuously solving differential equations. Sure. But when the differential equation tells them to screw that bolt here, they better screw that bolt here, or compromise the integrity of the bridge.
    - seanmcdirmid 13y ago
      Right, but how many mathematicians does it take to build a bridge? Probably just a few engineers, and the process is probably very standardize. That architect probably isn't using much math in his/her design. Software is similar: there is some math involved, but it is often abstracted away and you might not ever be exposed to it.
- brudgers 13y ago
  Software practice is more lenient than bridge building practice, but only by virtue of being so new as to escape regulation. There's nearly four fucking millennia worth of precedent for regulating construction because people die from blunders. The lack of accountability for the consequences of programs is unlikely to remain the context for practicing development. But even 25 years ago The Morris Worm was a treated as a felony and the list of actions for which there is criminal or civil liability has only grown. At some point normal programming activities will entail the risk of such liabilities to a degree that programming entails a formal standard of care like architecture and civil engineering and orthopedic surgery. https://en.m.wikipedia.org/wiki/Code_of_Hammurabi https://en.m.wikipedia.org/wiki/Code_of_Hammurabi

stiff 13y ago

Computers are formal systems as much as an alternating electrical current is a complex number, same with programming languages, even though both programming languages and formal systems can be viewed as abstract entities. Technically speaking all that can be said is that certain programming languages can be models for certain formal systems, and there is a big difference between being a model for a formal theory and something simply being only a formal theory: http://en.wikipedia.org/wiki/Reification_%28fallacy%29 http://en.wikipedia.org/wiki/Reification_%28fallacy%29 Programming language designers of most popular programming languages have no clue about neither denotational nor operational semantics and make use of no formal theory whatsoever. Anyhow, I do not deny the importance of various kinds of mathematics for programming, in some selected places and in the sense of writing programs that do mathematics. I am saying two things: - The attempts so far to turn programming itself into a single mathematical theory have failed miserably. Can you name one really important algorithm that was discovered by doing derivations in a formal axiomatic theory of programming? There is the "Algebra of programming" theory by Bird, the "Elements of programming" by Stepanov, but nothing particularly striking seems to ever come out of it, only proofs of things we already know. - There are hundreds of aspects of programming that have nothing to do with mathematics and turned out to be of far bigger importance than finding effective means of formal correctness proofs of programs. To give one example, programmers have to work in teams with the size of problems we are dealing with today, something the formal methods people never seemed to address much, and issues with communication and coordination cause much more problems than simple logical errors in algorithms.

loup-vaillant 13y ago
> Programming language designers of most popular programming languages have no clue about neither denotational nor operational semantics and make use of no formal theory whatsoever. That may explain why so many of our popular languages have several glaring flaws. Java doesn't support tail calls dammit! We had to wait for scheme to finally have lexical scope! C++ is impossible to parse! > The attempts so far to turn programming itself into a single mathematical theory have failed miserably. Wait, what attempts? I've read many Haskell papers, and did not stumble upon such a thing.

userbinator 13y ago

It feels like we're scared of abstractions. For instance, we solve linear equations every time we go to the grocery and pay cash. Yet being presented with those linear equations as such, get us running away screaming into the night. Because it is far easier to see value in solving real-world problems than to think in terms of just abstractions; and at the end of the day, real-world matters. Computers were invented for solving problems in reality, and that is one thing that should always be kept in mind when programming them. Abstractions, while powerful, also have a cost, both mentally and in terms of computing resources, and the latter is definitely finite, so being scared of them is both natural and reasonable. To put it bluntly, how many programmers don't know what "Curry-Howard correspondence", "first order logic", or "denotational and operational semantics" are, and yet have written hugely useful and popular applications? I argue that there is very little math and theory that one must know to do great things with programming - arithmetic and algebra are sufficient. So I believe we may see some truly wonderful things when we stop propagating this notion that computer science is hugely abstract maths, and instead focus on its more concrete aspects. (I touch on this point here too: https://news.ycombinator.com/item?id=7672252 https://news.ycombinator.com/item?id=7672252 )