4 ms·

Why would you call it "liberated"? Stuff like SmallTalk wouldn't be possible if programming was turned into math (and SmallTalk is way too cool by allowing cha

by bitL 11y ago

Why would you call it "liberated"? Stuff like SmallTalk wouldn't be possible if programming was turned into math (and SmallTalk is way too cool by allowing changing any part of its image on the fly and redefine all rules), and frankly I don't understand why mathematicians want to take over a completely different domain, computing. The relation between computing and math is more like the relation between physics and math. It's great to have multiple paradigms, why restrict oneself to a functional one when there is so much more?

jacobolus 11y ago
Note that this was the Turing Award lecture by John Backus, who created FORTRAN in the 1950s, and pretty much invented higher-level imperative programming. Before Backus, there was only machine code. Of course he was a mathematician: in those days “computing” didn’t exist as its own separate field. He can hardly be accused of “taking the domain over”.
- deleted 11y ago
  [deleted]
smosher_ 11y ago
> Stuff like SmallTalk wouldn't be possible if programming was turned into math > and frankly I don't understand why mathematicians want to take over a completely different domain I would like to challenge the assumption here: that programming (in whatever mode) can't be adequately described by mathematics. I don't have time to make a thorough argument, but consider this: instead of thinking of what programming would be like as some kind of math, think of what math would need to be like to adequately describe your favourite mode of programming. (Forget arithmetic, consider algebra, geometry.) As for FP: these days it wants all the tools, and it is picking up whatever it can formalize. Some FP tools are uncommon or don't work well outside the paradigm. To me that makes all the difference: I'd feel more restricted working without FP than by being strictly within it.
- eli_gottlieb 11y ago
  >I would like to challenge the assumption here: that programming (in whatever mode) can't be adequately described by mathematics. Well, the entire lesson of the Halting Problem and Rice's Theorem is that it can't. Indeed, Haskell loves to just cut through the bullshit about math and be inconsistent: bottom inhabits every type, and Type inhabits Type (in Dependent Haskell). No fixed mathematical system is capable of formally verifying all programs, or even all interesting programs. You always need more bits of axioms than of program if you want to prove theorems about your programs (Chaitin's principle, proved formally by Calude). What we can say for FP is that Fast and Loose Reasoning is Morally Correct, and that if we use nicely categorical constructions, then when our programs happen to terminate at all, those nice constructions describe their behavior.
  - Retra 11y ago
    We don't actually need to butt into the Halting Problem or Rices Theorem, though. Ideally, we would have proven-to-terminate non-turing complete DSLs that can be composed together to form more powerful DSLs. The problem is that we don't really know how to compose programs well, and when you demand the ability to peer into arbitrary executing code and modify it on the fly, you don't make it easier to learn how to do this. If you were forced to use an architecture that separated things properly, you'd be forced to deal with those composition problems, rather than 'hacking' programs using a level of power that is unnecessary for the problem you hope to solve. (And you are hoping to solve a problem, not just run a program that fails to terminate.) (I'm not arguing that this is the 'right way' to do things. It's just a way that should be considered properly.)
  - smosher_ 11y ago
    That's a little extreme. I think most computations are best¹ written in a way that is amenable to mathematical treatment, and most of the useful ones can be. Just because a counter-example exists doesn't mean we should give up hope. I find constructing programs mathematically makes life easier in the common case and possible in nearly all others, unless you insist on things like proof-of-termination for programs which do not (I do not.) 1. 'best' because it gives us the means to reason about the code, and we know what kind of transformations we can perform on it, and do them abstractly without having to simulate it, potentially for infinite inputs, etc., etc. You know the drill.

by bitL 11y ago

jacobolus 11y ago

Note that this was the Turing Award lecture by John Backus, who created FORTRAN in the 1950s, and pretty much invented higher-level imperative programming. Before Backus, there was only machine code. Of course he was a mathematician: in those days “computing” didn’t exist as its own separate field. He can hardly be accused of “taking the domain over”.

deleted 11y ago
[deleted]

smosher_ 11y ago

> Stuff like SmallTalk wouldn't be possible if programming was turned into math > and frankly I don't understand why mathematicians want to take over a completely different domain I would like to challenge the assumption here: that programming (in whatever mode) can't be adequately described by mathematics. I don't have time to make a thorough argument, but consider this: instead of thinking of what programming would be like as some kind of math, think of what math would need to be like to adequately describe your favourite mode of programming. (Forget arithmetic, consider algebra, geometry.) As for FP: these days it wants all the tools, and it is picking up whatever it can formalize. Some FP tools are uncommon or don't work well outside the paradigm. To me that makes all the difference: I'd feel more restricted working without FP than by being strictly within it.

eli_gottlieb 11y ago
>I would like to challenge the assumption here: that programming (in whatever mode) can't be adequately described by mathematics. Well, the entire lesson of the Halting Problem and Rice's Theorem is that it can't. Indeed, Haskell loves to just cut through the bullshit about math and be inconsistent: bottom inhabits every type, and Type inhabits Type (in Dependent Haskell). No fixed mathematical system is capable of formally verifying all programs, or even all interesting programs. You always need more bits of axioms than of program if you want to prove theorems about your programs (Chaitin's principle, proved formally by Calude). What we can say for FP is that Fast and Loose Reasoning is Morally Correct, and that if we use nicely categorical constructions, then when our programs happen to terminate at all, those nice constructions describe their behavior.
- Retra 11y ago
  We don't actually need to butt into the Halting Problem or Rices Theorem, though. Ideally, we would have proven-to-terminate non-turing complete DSLs that can be composed together to form more powerful DSLs. The problem is that we don't really know how to compose programs well, and when you demand the ability to peer into arbitrary executing code and modify it on the fly, you don't make it easier to learn how to do this. If you were forced to use an architecture that separated things properly, you'd be forced to deal with those composition problems, rather than 'hacking' programs using a level of power that is unnecessary for the problem you hope to solve. (And you are hoping to solve a problem, not just run a program that fails to terminate.) (I'm not arguing that this is the 'right way' to do things. It's just a way that should be considered properly.)
- smosher_ 11y ago
  That's a little extreme. I think most computations are best¹ written in a way that is amenable to mathematical treatment, and most of the useful ones can be. Just because a counter-example exists doesn't mean we should give up hope. I find constructing programs mathematically makes life easier in the common case and possible in nearly all others, unless you insist on things like proof-of-termination for programs which do not (I do not.) 1. 'best' because it gives us the means to reason about the code, and we know what kind of transformations we can perform on it, and do them abstractly without having to simulate it, potentially for infinite inputs, etc., etc. You know the drill.