> 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 hard to know what I don't know. I try to look at what people are doing/liking. But I feel confident that programming is inherently going to be about expressing the essence of the problem you're solving - a program will necessarily be as complex as the problem it's solving - and I think that limit is within reach of the approach I'm advocating, which is a conservative extrapolation of things we mostly already value. So I don't see the need to do anything more radical.
> 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.
A lot of the value of better programming would be new opportunities, not just cutting costs. I think the industry switching to Idris-level languages will bring a factor of 10 to 100 improvement in productivity - i.e. I expect we'll see companies of ~100 people putting the Google/Amazon/Citibanks out of business, and companies of less than 10 people competing heavily with the giants. That's the sort of thing technological improvements enable - compare the rate at which new videogames are being produced now, and how small the teams producing them are, or look at WhatsApp being treated as a serious competitive threat to Facebook with a staff of 10. I think there's been a lot of productivity gain recently that isn't fully captured in economic measures, because we've (rightly) become a lot more quality-of-life focused culturally, and so our productivity has gone into quality-of-life improvements that aren't so visible in GDP terms.
But I fully expect the transition to take decades, with good reason - I agree that a large company switching tomorrow wouldn't reap much benefit from Idris (though I do think we're at the stage where a technologically-aggressive startup should consider it).
> I don't see the need to do anything more radical.
I do, because the things that you mostly value (I guess I value them a lot less) seem to me incredibly complex for the good that they do, and we already have some alternatives that seem both more powerful and vastly simpler. But I am skeptical of them, too, though :)
> I think the industry switching to Idris-level languages will bring a factor of 10 to 100 improvement in productivity - i.e. I expect we'll see companies of ~100 people putting the Google/Amazon/Citibanks out of business, and companies of less than 10 people competing heavily with the giants.
That is a very powerful statement, and I'd like to know why you'd think that. I would even like to know what makes you think that any language (never mind which) can make such an impact, even though we've seen nothing of this sort. I do not share your belief that Idris could make such an impact or anywhere near it, nor probably any other language.
I am skeptical, because having looked at Idris and played with it a bit, I was completely underwhelmed. Java + JML can do pretty much the same, if not better, and for a lowe cost, and this is not a statement about Java+JML being a leap forward. I have no idea if Eve could make an impact as big as the one you predict, but at least I don't feel I can instinctively reject this possibility as easily as I could Idris, as Eve actually brings a lot of new things to the table, where Idris feels like some ergonomic improvement over things that may have had some potential that never materialized, in the hope that better ergonomics is what should do it.
I would like to point out one more problem with viewing the abundance of research as a proxy for utility or of an "established idea", one that touches on my own personal biases :) When you publish a paper, certainly in good journals/conferences, you must exhibit some significant novelty. This, ironically, rewards the more complicated (and so arguably less useful in the real world) frameworks and punishes the simpler ones. For example, I've seen papers talking about embedding separation logic, or specifying amortized worst-case complexity in Coq. You won't see such papers on TLA, because doing both in TLA is rather trivial. Lamport himself complained that he had trouble publishing a paper on specifying and verifying realtime systems in TLA because it is so straightforward that it was hard to demonstrate mathematical novelty. He had to artificially add an extra novelty (the use of a model checker) to make the paper worthy of publication [1].
> That is a very powerful statement, and I'd like to know why you'd think that. I would even like to know what makes you think that any language (never mind which) can make such an impact, even though we've seen nothing of this sort.
I think we have; I think we've seen dramatically accelerating programmer productivity. I think language improvements compound heavily: if a language is slightly more efficient in the small, that means code has to be broken up less, which give it more and more of an efficiency advantage as the codebase gets larger.
> I am skeptical, because having looked at Idris and played with it a bit, I was completely underwhelmed. Java + JML can do pretty much the same, if not better, and for a lowe cost, and this is not a statement about Java+JML being a leap forward. I have no idea if Eve could make an impact as big as the one you predict, but at least I don't feel I can instinctively reject this possibility as easily as I could Idris, as Eve actually brings a lot of new things to the table, where Idris feels like some ergonomic improvement over things that may have had some potential that never materialized, in the hope that better ergonomics is what should do it.
All of programming language design could be called ergonomic improvements. I always found all the pre/post contract stuff too complicated and too different from normal programming to get any value out of; being able to capture more in plain old functions, values and types is where I see value.
> I think we've seen dramatically accelerating programmer productivity.
Really? I think that the change that has contributed to the lion's share of that boost has nothing to do with language features, and has everything to do with the availability of open-source libraries. The other major contributions have been the widespread adoption of automated unit tests -- also not a language feature, and the practicality of GCs -- if considered a language feature, it's a transparent one.
When Brooks said, around '85, I think, that we won't see a single improvement contributing to a 10x improvement within a single decade, people said he was pessimistic. After 30 years I don't think we've seen a 10x improvement with all methods combined, and if we have, most of it is due to libraries.
Do you think that writing, say, an ERP, a power-station control and management software or an air-traffic control system from scratch (without off-the-shelf/open-source libraries) today would be 10x less costly than it was using C++ in 1987, or even 3x less costly than using Java in 2002 (I'm taking 30 and 15 years respectively as milestones)? Remeber that 10x within a decade was seen as pessimistic.
Although I was just a novice programmer in 1987, I think that the answer to both is an emphatic no. Even when it comes to small/simple programs (which are a completely separate domain), I'm pretty sure that aside from the availability of libraries, Python doesn't have even a 3x factor over VB/Delphi/other "RAD" languages, as they were called way back when.
> Do you think that writing, say, an ERP, a power-station control and management software or an air-traffic control system from scratch (without off-the-shelf/open-source libraries) today would be 10x less costly than it was using C++ in 1987, or even 3x less costly than using Java in 2002 (I'm taking 30 and 15 years respectively as milestones)? Remeber that 10x within a decade was seen as pessimistic.
I'd want to amend that to no domain-specific libraries - I think part of the language advantage is making very general libraries possible. But yes, I do think writing such a system to the same standard would be better than 3x cheaper than in 2002. (I don't think that's what would be done - our implicit expectations around software usability are very different today to what they were in 2002. But I do think we'd get more than 3x better value for the same money than in 2002, certainly risk-adjusted - I think in 2002 there would have been a substantial chance that the project would fail outright)
For smaller programs I'd agree that we haven't improved that much, although it's very difficult to talk about how hard it would be to write small programs without libraries because small programs are mostly just using libraries.
It's hard to know what I don't know. I try to look at what people are doing/liking. But I feel confident that programming is inherently going to be about expressing the essence of the problem you're solving - a program will necessarily be as complex as the problem it's solving - and I think that limit is within reach of the approach I'm advocating, which is a conservative extrapolation of things we mostly already value. So I don't see the need to do anything more radical.
> 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.
A lot of the value of better programming would be new opportunities, not just cutting costs. I think the industry switching to Idris-level languages will bring a factor of 10 to 100 improvement in productivity - i.e. I expect we'll see companies of ~100 people putting the Google/Amazon/Citibanks out of business, and companies of less than 10 people competing heavily with the giants. That's the sort of thing technological improvements enable - compare the rate at which new videogames are being produced now, and how small the teams producing them are, or look at WhatsApp being treated as a serious competitive threat to Facebook with a staff of 10. I think there's been a lot of productivity gain recently that isn't fully captured in economic measures, because we've (rightly) become a lot more quality-of-life focused culturally, and so our productivity has gone into quality-of-life improvements that aren't so visible in GDP terms.
But I fully expect the transition to take decades, with good reason - I agree that a large company switching tomorrow wouldn't reap much benefit from Idris (though I do think we're at the stage where a technologically-aggressive startup should consider it).