|
|
|
|
|
by pron
3675 days ago
|
|
Give me Java and a real-world problem vs someone using using Scala and I will beat them on the initial write, and destroy them on the maintenance. :) > in five years' time I'm sure Idris will be a better language than Scala Idris? In the entire history of computing there has been a single[1] complete non-trivial (though still rather small) real-world program (CompCert) written in a dependently typed language. Even though the program is small and the programmer (Xavier Leroy) one of the leading dependent-type-based-verification experts, the effort was big (and that's an understatement) and the termination proofs proved too hard/tedious for him, so he just used a simple counter for termination and had a runtime exception if it ran out. Idris is a very interesting experiment, I'll give you that. But I don't see how anyone can be sure that it would work (although you didn't say it can work, only that it would "be a better language than Scala", so I'm not sure what your success metrics are). [1]: Approximately, though I don't know of any other. |
|
Seems we have a true disagreement.
> Idris? In the entire history of computing there has been a single[1] complete non-trivial (though still rather small) real-world program (CompCert) written in a dependently typed language.
Five or ten years ago how many such programs were there in a language with higher-kinded types? Thirty years ago how many with type inference? Innovation is slow - perhaps five years was too optimistic, looking at the history - but it does happen; PLT ideas do eventually make their way into mainstream languages.
> although you didn't say it can work, only that it would "be a better language than Scala", so I'm not sure what your success metrics are
I think it will be the most effective (for real-world problems) general-purpose programming language - a spot I think Scala currently holds. Hard to define objectively of course.