> When your constraints mean that only the right thing can be done, you can make the thing implicit.
Except that sometimes, when you think about the practical issue long and hard enough, you can find that some constraints need not be stated at all, and can be completely factored out of the language, at least in most cases. For example, GC removes resource management out of the equation (it's not always the right solution, but it is the right one in a large enough portion of software). Or, while FP people pore over effect systems and how to constrain effect, languages like Eve that adopt synchronous programming (which is based on ideas from temporal logic), get a mathematical framework in which effects and computation are one and the same, and effects don't pose a challenge to begin with.
> I actually think that gradient ascent from Java will happen, and will move the industry forward
Perhaps, but I doubt it's in the direction pointed to by Idris. We have much better ideas around. The author of the slides mentioned only the segment of PL research that he find appealing. Other segments may have some more promising ideas.
> I think we can go at least one or two substantial steps better than Idris: I want Noether's levels of stratification (beyond just total/not-provably-total), and I want Rust-style linearity, not as a specialised capability but as something integrated into the regular type system. But even if Idris is the limit, it's still a big step ahead of Java, and it's going to take the industry a while to make that step.
I think you have fallen in love with a specific formalism (I've fallen in love with others) and can only see progress within it. If you take a step back, ignore formalism altogether and ask yourself -- or better yet, conduct research -- on what are the actual problems in programming, you may find solutions in completely different directions.
> it's still a big step ahead of Java
I don't think so, and I don't know why you'd think that. I'm not even sure that Java isn't the limit (modulo small improvements). Of course, when I say something is a big step ahead I don't mean that I enjoy it more or that it can pull some more technical tricks, but rather that it reduces development costs by 30%. If Idris is a big step ahead of Java, by how much do you think costs at, say, Google or Amazon or Citibank would drop if they decided they would all switch to Idris tomorrow? I'm fairly certain that it wouldn't be anywhere near 30%, and I'm not even sure costs wouldn't actually rise.
> it feels like most of the industry is only just adopting the things that OCaml offered, and not yet familiar enough with them to appreciate what Haskell offers above that.
I see it not as progress but as change in fashion. Tastes change, and so people adopt some ideas. Have productivity levels risen in the past three decades? Significantly less so than even Brooks's prediction, which was considered overly pessimistic.
Except that sometimes, when you think about the practical issue long and hard enough, you can find that some constraints need not be stated at all, and can be completely factored out of the language, at least in most cases. For example, GC removes resource management out of the equation (it's not always the right solution, but it is the right one in a large enough portion of software). Or, while FP people pore over effect systems and how to constrain effect, languages like Eve that adopt synchronous programming (which is based on ideas from temporal logic), get a mathematical framework in which effects and computation are one and the same, and effects don't pose a challenge to begin with.
> I actually think that gradient ascent from Java will happen, and will move the industry forward
Perhaps, but I doubt it's in the direction pointed to by Idris. We have much better ideas around. The author of the slides mentioned only the segment of PL research that he find appealing. Other segments may have some more promising ideas.
> I think we can go at least one or two substantial steps better than Idris: I want Noether's levels of stratification (beyond just total/not-provably-total), and I want Rust-style linearity, not as a specialised capability but as something integrated into the regular type system. But even if Idris is the limit, it's still a big step ahead of Java, and it's going to take the industry a while to make that step.
I think you have fallen in love with a specific formalism (I've fallen in love with others) and can only see progress within it. If you take a step back, ignore formalism altogether and ask yourself -- or better yet, conduct research -- on what are the actual problems in programming, you may find solutions in completely different directions.
> it's still a big step ahead of Java
I don't think so, and I don't know why you'd think that. I'm not even sure that Java isn't the limit (modulo small improvements). Of course, when I say something is a big step ahead I don't mean that I enjoy it more or that it can pull some more technical tricks, but rather that it reduces development costs by 30%. If Idris is a big step ahead of Java, by how much do you think costs at, say, Google or Amazon or Citibank would drop if they decided they would all switch to Idris tomorrow? I'm fairly certain that it wouldn't be anywhere near 30%, and I'm not even sure costs wouldn't actually rise.
> it feels like most of the industry is only just adopting the things that OCaml offered, and not yet familiar enough with them to appreciate what Haskell offers above that.
I see it not as progress but as change in fashion. Tastes change, and so people adopt some ideas. Have productivity levels risen in the past three decades? Significantly less so than even Brooks's prediction, which was considered overly pessimistic.