3 ms·

There is more cult than cult leader. The people who enjoy functional programming find it vastly enjoyable/better/whatever. I fully admit it's hard to convey thi

There is more cult than cult leader. The people who enjoy functional programming find it vastly enjoyable/better/whatever. I fully admit it's hard to convey this and hard to demonstrate this empirically because the cost and scale of an adequate experiment would be prohibitive. The biggest thing I don't like about the model checkers and other strategies is: 1. No separation of proof and proof search. Deductive proofs are a good lingua franca. I want to mix and match techniques to derive the proofs and have them work together. Many of the things you like have potential to be repurposed as such "tactics". 2. Composition of verified programs. Functional programers really value composition and the things you like tend to be used for "whole progra verification". At the very least, while one can verify individual parts, there is no mechanized way to combine those proofs. I also think the evidence already points away from your scale argument. To put it simply, right now Agda is good for toy stuff, things you like are good for medium stuff, but only Coq and Isabelle/HOL is used for the biggest projects like Cake ML and Comp Cert. Both of those are proof theoretic tools.

nosianu 7y ago
> The people who enjoy functional programming find it vastly enjoyable/better/whatever. That's a tautology... Anyway.... I think I "get" enough of FP and I use parts of it. I certainly find it very useful. Types as well, very useful for me. However, headlines like the current one and comments along the same hype line are just annoying. I sure like practical people discussing these things, but reality in this universe is that if you actually want to do something in the real world there is no abstraction that's even close to complete. Everything leaks like a sieve. You compensate by choosing and mixing your tools and by adapting on the fly. Theory is a tool, nothing more. "I'm a functional programmer" - okay, I'm merely a "programmer", and I choose whatever works best and don't fuzz about labels and purity. The points you mention all work in parts, and disintegrate in other parts when they come into contact with a real problem plus its context. These discussions are so... random and often emotional and committed because there is no context to measure against. It's just words. If there is a concrete problem including the concrete context (the entire environment and business context) it's much easier to agree on something. Without that, every commenter comes in with their own context vision in their brain, which depends on what they've been doing. In the end any non-trivial piece of engineering (software or not) is much more messy than any theory can account for. Exactly what @pron said in the comment you replied to about the "Appeals to "the power of math"" akin to a believe in magical solutions. I find it extremely pretentious TBO, although I certainly value math very highly. But it's a tool with severe limitations and not a magical instrument. All this stuff - math, type systems, FP - appear to us so "pure" and as the perfect solution because we invented it and (also because of that) it is a great match for how our brain works: Which means disregarding 99% of reality (and our sensors are very limited to begin with). But whenever we try to apply a thus derived "pure" solution to the real world we find that the disregarded and filtered-out aspects start appearing in all corners. If the person looking at it also has the same bias they concentrate on only the part that was successfully modeled and think "this worked perfectly", so in evaluating the solution you have the same filter again. But whenever you try to do something more complex and/or more complete with math it's a major undertaking, taking many very good people a long time. So yes, math can be used to model more aspects, but that results in an explosion of complexity. The closer you program on "math space" problems the more perfect the mathy solutions like FP and type systems will fit. The more the real world has to be dealt with the more the leaks in the abstractions will become apparent. You can try to deal with them with the "mathy" solutions to remain in that space, but that then becomes more and more complex, and at some point you end up with a "hack" to cut through the thicket. I highly recommend learning the basics of (cell-level and below) biology and biochemistry instead of yet another programming language to see a very different system. Then it becomes apparent the differences between various programming tools are much less than the heated discussion make it seem. When you look with a magnifier glass tiny differences look like mountains. FP, OOP, procedural programming, whatever - it's all not all that different really, in comparison. It should be more apparent when you remember it all runs on the exact kind of hardware architecture. Our computing hardware is not diverse at all really (quantum computing as a very early and very limited experiment being a noteworthy exception; as are mostly older analog computing systems). The layers on top are all closely bound by and to it.
- Ericson2314 7y ago
  There's loads to respond to here, but let me just say > Everything leaks like a sieve. Not in my experience. I, for work, use 100% Haskell (well, and some SQL) mainly to write web apps. Not "math space" problems by any means. We use and have written many abstractions. None of them are particularly leaky. Some of have implementations I don't thoroughly understand and yet have no trouble using anyways---I no no better way to demonstrate a lack of leaks than that.
- Ericson2314 7y ago
  > That's a tautology.. It almost is, except for "vastly". I'm saying there isn't very many people who enjoy it but find it in their experience merely slightly better.
pron 7y ago
> I fully admit it's hard to convey this and hard to demonstrate this empirically because the cost and scale of an adequate experiment would be prohibitive. Ah, but you see, here we have a problem. If you claim that your favorite technique has a big measurable impact on software development costs, then observing them shouldn't be hard at all, even without careful empirical studies. There are many problems with free markets, but applying selection pressures that quickly pick adaptive techniques is something markets are actually good at. And if your claim is that the benefit is not easily measurable because it's not so large and decisive, then why is your claim important at all? And, BTW, I think the preference for a programming style is very personal. I learned and used FP before I learned OOP, and I like both (maybe for different things), but I can't say I have such a strong preference for either. They're both OK. > but only Coq and Isabelle/HOL is used for the biggest projects like Cake ML and Comp Cert. Both of those are proof theoretic tools. Coq and Isabelle have so far only been used to verify deep properties of tiny programs, up to ~10KLOC; that's 1/5 of jQuery. Even then the effort was huge. Model checkers have been used on much larger programs, and, at least for small programs, they're commonly and regularly used in industry (especially in safety-critical hard realtime systems).
- lmm 7y ago
  > If you claim that your favorite technique has a big measurable impact on software development costs, then observing them shouldn't be hard at all, even without careful empirical studies. There are many problems with free markets, but applying selection pressures that quickly pick adaptive techniques is something markets are actually good at. I'm not convinced this is true in an environment where every problem is unique and failure rates are already high - humans are known to be very bad at working with low probabilities. Even if we're talking about an order-of-magnitude difference, who could distinguish between a startup - or an internal new project - with a 1.5% success rate versus a 15% success rate? That goes doubly when we're talking about costs: a friend who'd worked for several investment banks observed that they all had roughly the same number of developers overall, but the distribution of those developers was radically different: bank X would have 5 programmers working in area A and 50 programmers working in area B, while bank Y would have the opposite, even though both were solving the same problem in area A and area B. Could you tell whether Google or Facebook has 500 or 5000 or 50000 developers from the outside? Does Uber have 50 or 500 or 5000? (I genuinely don't know). To my mind the most compelling case: WhatsApp apparently did succeed with an order of magnitude fewer developers than comparable companies - and the industry responded with a collective shrug. (My interpretation is that the industry is still so immature - or so fast-moving - that an order of magnitude cost saving still doesn't matter; software produced at 10x what it "should" cost can still be amply productive/profitable, it's easier to increase profits by increasing revenue than by cutting costs).

nosianu 7y ago

> The people who enjoy functional programming find it vastly enjoyable/better/whatever. That's a tautology... Anyway.... I think I "get" enough of FP and I use parts of it. I certainly find it very useful. Types as well, very useful for me. However, headlines like the current one and comments along the same hype line are just annoying. I sure like practical people discussing these things, but reality in this universe is that if you actually want to do something in the real world there is no abstraction that's even close to complete. Everything leaks like a sieve. You compensate by choosing and mixing your tools and by adapting on the fly. Theory is a tool, nothing more. "I'm a functional programmer" - okay, I'm merely a "programmer", and I choose whatever works best and don't fuzz about labels and purity. The points you mention all work in parts, and disintegrate in other parts when they come into contact with a real problem plus its context. These discussions are so... random and often emotional and committed because there is no context to measure against. It's just words. If there is a concrete problem including the concrete context (the entire environment and business context) it's much easier to agree on something. Without that, every commenter comes in with their own context vision in their brain, which depends on what they've been doing. In the end any non-trivial piece of engineering (software or not) is much more messy than any theory can account for. Exactly what @pron said in the comment you replied to about the "Appeals to "the power of math"" akin to a believe in magical solutions. I find it extremely pretentious TBO, although I certainly value math very highly. But it's a tool with severe limitations and not a magical instrument. All this stuff - math, type systems, FP - appear to us so "pure" and as the perfect solution because we invented it and (also because of that) it is a great match for how our brain works: Which means disregarding 99% of reality (and our sensors are very limited to begin with). But whenever we try to apply a thus derived "pure" solution to the real world we find that the disregarded and filtered-out aspects start appearing in all corners. If the person looking at it also has the same bias they concentrate on only the part that was successfully modeled and think "this worked perfectly", so in evaluating the solution you have the same filter again. But whenever you try to do something more complex and/or more complete with math it's a major undertaking, taking many very good people a long time. So yes, math can be used to model more aspects, but that results in an explosion of complexity. The closer you program on "math space" problems the more perfect the mathy solutions like FP and type systems will fit. The more the real world has to be dealt with the more the leaks in the abstractions will become apparent. You can try to deal with them with the "mathy" solutions to remain in that space, but that then becomes more and more complex, and at some point you end up with a "hack" to cut through the thicket. I highly recommend learning the basics of (cell-level and below) biology and biochemistry instead of yet another programming language to see a very different system. Then it becomes apparent the differences between various programming tools are much less than the heated discussion make it seem. When you look with a magnifier glass tiny differences look like mountains. FP, OOP, procedural programming, whatever - it's all not all that different really, in comparison. It should be more apparent when you remember it all runs on the exact kind of hardware architecture. Our computing hardware is not diverse at all really (quantum computing as a very early and very limited experiment being a noteworthy exception; as are mostly older analog computing systems). The layers on top are all closely bound by and to it.

Ericson2314 7y ago
There's loads to respond to here, but let me just say > Everything leaks like a sieve. Not in my experience. I, for work, use 100% Haskell (well, and some SQL) mainly to write web apps. Not "math space" problems by any means. We use and have written many abstractions. None of them are particularly leaky. Some of have implementations I don't thoroughly understand and yet have no trouble using anyways---I no no better way to demonstrate a lack of leaks than that.
Ericson2314 7y ago
> That's a tautology.. It almost is, except for "vastly". I'm saying there isn't very many people who enjoy it but find it in their experience merely slightly better.

pron 7y ago

> I fully admit it's hard to convey this and hard to demonstrate this empirically because the cost and scale of an adequate experiment would be prohibitive. Ah, but you see, here we have a problem. If you claim that your favorite technique has a big measurable impact on software development costs, then observing them shouldn't be hard at all, even without careful empirical studies. There are many problems with free markets, but applying selection pressures that quickly pick adaptive techniques is something markets are actually good at. And if your claim is that the benefit is not easily measurable because it's not so large and decisive, then why is your claim important at all? And, BTW, I think the preference for a programming style is very personal. I learned and used FP before I learned OOP, and I like both (maybe for different things), but I can't say I have such a strong preference for either. They're both OK. > but only Coq and Isabelle/HOL is used for the biggest projects like Cake ML and Comp Cert. Both of those are proof theoretic tools. Coq and Isabelle have so far only been used to verify deep properties of tiny programs, up to ~10KLOC; that's 1/5 of jQuery. Even then the effort was huge. Model checkers have been used on much larger programs, and, at least for small programs, they're commonly and regularly used in industry (especially in safety-critical hard realtime systems).

lmm 7y ago
> If you claim that your favorite technique has a big measurable impact on software development costs, then observing them shouldn't be hard at all, even without careful empirical studies. There are many problems with free markets, but applying selection pressures that quickly pick adaptive techniques is something markets are actually good at. I'm not convinced this is true in an environment where every problem is unique and failure rates are already high - humans are known to be very bad at working with low probabilities. Even if we're talking about an order-of-magnitude difference, who could distinguish between a startup - or an internal new project - with a 1.5% success rate versus a 15% success rate? That goes doubly when we're talking about costs: a friend who'd worked for several investment banks observed that they all had roughly the same number of developers overall, but the distribution of those developers was radically different: bank X would have 5 programmers working in area A and 50 programmers working in area B, while bank Y would have the opposite, even though both were solving the same problem in area A and area B. Could you tell whether Google or Facebook has 500 or 5000 or 50000 developers from the outside? Does Uber have 50 or 500 or 5000? (I genuinely don't know). To my mind the most compelling case: WhatsApp apparently did succeed with an order of magnitude fewer developers than comparable companies - and the industry responded with a collective shrug. (My interpretation is that the industry is still so immature - or so fast-moving - that an order of magnitude cost saving still doesn't matter; software produced at 10x what it "should" cost can still be amply productive/profitable, it's easier to increase profits by increasing revenue than by cutting costs).