Earlier quoted context omitted.
> 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 solu…
> 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 solv…
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].
[1]: http://lamport.azurewebsites.net/pubs/pubs.html#real-simple