4 ms·

> If in the next fifty years more than, say, 3% of programmers will be programming in a language like Lean, I will eat my hat. You're not even putting any stak

> If in the next fifty years more than, say, 3% of programmers will be programming in a language like Lean, I will eat my hat. You're not even putting any stakes on the table. That's such a safe bet. It's unlikely you'd even have a chance at losing the odds are so stacked. There's a great talk on why functional programming is not the norm: https://www.youtube.com/watch?v=QyJZzq0v7Z4 https://www.youtube.com/watch?v=QyJZzq0v7Z4 The short of it is: network effects. Haskell, OCaml, SML... they've never had the benefit of being the exclusive language to a popular platform like the web, macOS, or UNIX. They've not yet had a killer app like Rails or Numpy/SciPy/PyTorch. They've certainly not been foisted on the market with a war chest of marketing dollars like Java and C#. And they're not an incremental improvement on the status quo with an obvious, easy benefit. > Now, try to explain to a programmer what kind of object id is That's a rhetorical exercise. You can take a random snippet of APL or Fortran and the outcome would be the same. Every language requires training and effort to learn. I teach people Haskell and TLA+. If you think teaching people the value of a language like Haskell is hard you should see the blank stares I get on the first day teaching experienced developers TLA+. Interested folks will come around eventually and have their moment but it takes training and dedication to get there. > was chosen not with the best interests of programmers in mind I'm well aware. I converse regularly with the maintainers of mathlib and the community. I know the focus there is on building a good tool for mathematicians. I still think they built an interesting programming language even if that wasn't their intended purpose. That's why I started writing the hackers' guide. The documentation on the programming side is missing and needs to be filled in. They still need programmers to build the tools, the VM, the libraries, etc. It's niche. And I'm not even the least bit surprised you find it horrible. I don't expect Lean to take off with programmers. I think the ideas in it are good and there is definitely some good things we could take from it in designing the dependently typed programming language that does penetrate the market and over-come the network effects. Either way I think the people proposing the challenges for Haskell programmers to solve have a good reason to do so otherwise we would have a hard time finding the motivation for it. We want to see where algebraic effects go because new users often complain that monad transformers are hard to learn and users of mtl cite many problems that a well-done algebraic effect system would alleviate. Dependent types would remove the complexity of writing programs that work with types and enable us to write more programs with more expressive types. If you don't see why that's useful then what do you think the community should be focusing on?

pron 7y ago
> There's a great talk on why functional programming is not the norm It's a great talk in the sense that it satisfies people who want excuses. The real reason is similar to the one in the talk, but more disappointing: over decades, functional programming was not found to be either significantly better or significantly worse than other paradigms in productivity or other similar metrics, but for many years imperative paradigms enjoyed a significant benefit in runtime performance, and so there's really no reason to switch. I honestly couldn't care -- I like, and hate, OOP and FP equally -- but paradigms exist to serve practitioners, not the other way around. One thing is clear: you cannot at once say you're interested in serving the research of typed lambda calculus -- a worthy research goal -- and also in advancing the state-of-the-art in the software industry, which is another worthy goal, but a very different one. If you're interested in the latter you must conduct some sort of study on the problem at hand; if you're interested in the former, then you have zero information to make a claim about the latter. In other words, you can either want to advance programming or advance typed FP; you cannot do both at once, because doing they both require very different kinds of study. If you're for typed FP, then that position is no less valid than being for OOP, or any other paradigm some people like, but it's not more valid, either. > And they're not an incremental improvement on the status quo with an obvious, easy benefit. ... or at all. > That's a rhetorical exercise. You can take a random snippet of APL or Fortran and the outcome would be the same. I totally disagree here. Simplifying ideas makes you understand what is essential and what isn't, and is absolutely required before some idea can get out of the lab and become a useful technology in the field. If the most basic subroutine represents some object in a meta-universe, that even 99% of mathematicians have no clue about -- you're off to a bad start with engineers. The use of constructive type theory as a foundation is interesting to logicians who want to study the properties of constructive type theories and of proof assistants based on them. It is nothing but an unnecessary complication for software developers. As you point out, there are often some necessary complications, so there's really no need to add unnecessary ones. BTW, you mentioned TLA+. TLA+ also requires some effort, although significantly less than Lean (or Isabelle, or Coq), but TLA+ has made a historical breakthrough in formal logic. From its inception in the late 19th century, and even from its first beginnings in the 17th, formal logic aspired to be a useful tool for practitioners. But time and again it's fallen far short of that goal, something that logicians like John von Neumann and Alan Turing bemoaned. AFAIK, TLA+ is the first powerful (i.e. with arbitrary quantification) formal logic in the history of formal logic that has gained some use among ordinary practitioners -- to paraphrase Alan Turing, among "the programmers in the street" (Turing said that formal logic failed to find use for "the mathematician in the street," and tried, unsuccessfully, to rectify that). It was no miracle: Lamport spent years trying to simplify the logic and adapt it to the actual needs of engineers, including through "field research" (others, like David Harel, have done the same). That is something that the logicians behind other proof assistants seem to be uninterested in doing, and so their failure in achieving that particular goal is unsurprising. > Every language requires training and effort to learn. ... Interested folks will come around eventually and have their moment but it takes training and dedication to get there. But why get there at all? I'm interested, I learned some Haskell and some Lean, I think Haskell is OK -- not much better or much worse than most languages, but not my cup of tea -- and Lean is very interesting for those interested in formal logic, but offers little to engineers; I enjoy it because I'm interested in some theoretical aspects. But why would I subject other developers who aren't particularly interested in a certain paradigm to suffer until they "get there" just for the sake of that paradigm? Again, paradigms exist to serve practitioners, not the other way around. > If you don't see why that's useful then what do you think the community should be focusing on? I think the community should be honest about what Haskell is: a testing ground for ideas in the research of typed functional programming. Then, it should consider measuring some results before disappearing down its own rabbit hole, where it's of little use to anyone. Algebraic effects could be an interesting experiment at this point. I don't really care about the pains of all 300 Haskell developers with monad transformers, but if Haskell tries another approach to IO, then it might eventually find a generally useful ones; same goes for using linear types instead of monads. But dependent types? They're currently at the stage when even their biggest fans find it hard to say more good things about them than bad. If Haskell wants to serve software by testing out new ideas in typed functional programming, I think it should at least focus on ones that might still be in the lab but are at least out of the tube.

pron 7y ago

> There's a great talk on why functional programming is not the norm It's a great talk in the sense that it satisfies people who want excuses. The real reason is similar to the one in the talk, but more disappointing: over decades, functional programming was not found to be either significantly better or significantly worse than other paradigms in productivity or other similar metrics, but for many years imperative paradigms enjoyed a significant benefit in runtime performance, and so there's really no reason to switch. I honestly couldn't care -- I like, and hate, OOP and FP equally -- but paradigms exist to serve practitioners, not the other way around. One thing is clear: you cannot at once say you're interested in serving the research of typed lambda calculus -- a worthy research goal -- and also in advancing the state-of-the-art in the software industry, which is another worthy goal, but a very different one. If you're interested in the latter you must conduct some sort of study on the problem at hand; if you're interested in the former, then you have zero information to make a claim about the latter. In other words, you can either want to advance programming or advance typed FP; you cannot do both at once, because doing they both require very different kinds of study. If you're for typed FP, then that position is no less valid than being for OOP, or any other paradigm some people like, but it's not more valid, either. > And they're not an incremental improvement on the status quo with an obvious, easy benefit. ... or at all. > That's a rhetorical exercise. You can take a random snippet of APL or Fortran and the outcome would be the same. I totally disagree here. Simplifying ideas makes you understand what is essential and what isn't, and is absolutely required before some idea can get out of the lab and become a useful technology in the field. If the most basic subroutine represents some object in a meta-universe, that even 99% of mathematicians have no clue about -- you're off to a bad start with engineers. The use of constructive type theory as a foundation is interesting to logicians who want to study the properties of constructive type theories and of proof assistants based on them. It is nothing but an unnecessary complication for software developers. As you point out, there are often some necessary complications, so there's really no need to add unnecessary ones. BTW, you mentioned TLA+. TLA+ also requires some effort, although significantly less than Lean (or Isabelle, or Coq), but TLA+ has made a historical breakthrough in formal logic. From its inception in the late 19th century, and even from its first beginnings in the 17th, formal logic aspired to be a useful tool for practitioners. But time and again it's fallen far short of that goal, something that logicians like John von Neumann and Alan Turing bemoaned. AFAIK, TLA+ is the first powerful (i.e. with arbitrary quantification) formal logic in the history of formal logic that has gained some use among ordinary practitioners -- to paraphrase Alan Turing, among "the programmers in the street" (Turing said that formal logic failed to find use for "the mathematician in the street," and tried, unsuccessfully, to rectify that). It was no miracle: Lamport spent years trying to simplify the logic and adapt it to the actual needs of engineers, including through "field research" (others, like David Harel, have done the same). That is something that the logicians behind other proof assistants seem to be uninterested in doing, and so their failure in achieving that particular goal is unsurprising. > Every language requires training and effort to learn. ... Interested folks will come around eventually and have their moment but it takes training and dedication to get there. But why get there at all? I'm interested, I learned some Haskell and some Lean, I think Haskell is OK -- not much better or much worse than most languages, but not my cup of tea -- and Lean is very interesting for those interested in formal logic, but offers little to engineers; I enjoy it because I'm interested in some theoretical aspects. But why would I subject other developers who aren't particularly interested in a certain paradigm to suffer until they "get there" just for the sake of that paradigm? Again, paradigms exist to serve practitioners, not the other way around. > If you don't see why that's useful then what do you think the community should be focusing on? I think the community should be honest about what Haskell is: a testing ground for ideas in the research of typed functional programming. Then, it should consider measuring some results before disappearing down its own rabbit hole, where it's of little use to anyone. Algebraic effects could be an interesting experiment at this point. I don't really care about the pains of all 300 Haskell developers with monad transformers, but if Haskell tries another approach to IO, then it might eventually find a generally useful ones; same goes for using linear types instead of monads. But dependent types? They're currently at the stage when even their biggest fans find it hard to say more good things about them than bad. If Haskell wants to serve software by testing out new ideas in typed functional programming, I think it should at least focus on ones that might still be in the lab but are at least out of the tube.