I'd rate Elixir right now only as "up-and-coming". It is not yet an acceptable second-tier choice. Even in an environment where Ruby or Python (or the several other similar second-tier languages) are accepted without a second thought (as opposed to an environment where only first-tiers like Java or C(#/++/) are acceptable), Elixir will still result in some questions being asked that you better have a good answer for.
This is not a criticism of the language, simply descriptive of its current position. Go, which is substantially larger at the moment from what I can see, is just barely cracking that boundary that I described, and probably still has a good year or two before it's quite there.
Elixir is currently on a good trajectory, but I would definitely be concerned that trying to be a Ruby on top of the Erlang VM is going to make it a non-trivial challenge to get to the next level of usage, precisely because the Ruby space is covered, covered, and covered again with mature, existing languages. This is, again, not a promise from me it can't succeed, indeed I wish it all the best, just a description of its challenges. It is growing rapidly in its little niche but it may have a serious challenge getting to the next level.
And, back on topic, when this came up on Reddit, I'd observe that Elixir is the only dynamically-typed "up-and-coming" language I can think of. Nim is statically-typed. Rust is static. Go is probably on the way out of "up-and-coming" but it's static.
I also observe that all the dynamic languages are all adding static type support, even when the static type support is inevitably compromised by the dynamic portion of the language. In the meantime, I don't see any static language trying to move in a dynamic direction... in fact, many of the static languages are moving to be even more static! The net flow of feature work right now is strongly in the static direction.
Point. And it's a non-trivial implementation, from the look of it. A lot of static languages have "a thing that can be passed around as a 'dynamic' value but has to be cast back to a static type to do anything", but the C# feature is much more than that.
Also, I observe on the docs page this little note that says "As of Scala 2.10, defining direct or indirect subclasses of this trait is only possible if the language feature 'dynamics' is enabled."
Almost all the static languages have some sort of dynamic feature already, and generally have since day one. The mere existence of "dynamic" features isn't my point. The question is, how often are they used, and is the language tending towards more of them or less of them? I don't do Scala, so I can't speak to it, but does every little Scala program use this dynamic package, or is it something rarely reached for, and even perhaps considered a code smell by the community? If it's the latter, then it's not a huge notch in the "dynamic" belt.
I'm discussing the first derivative, not the current state of the world.
I don't think it's considered a code smell, but it is intended to be used only for cases where the problem your modelling really is dynamic. Basically, in cases where you end up having classes that have methods like
def lookup(name: String): Any
you can instead use Dynamic, meaning instead of having calls like this:
myObj.lookup("foo")
you can do this:
myObj.foo
So no, Scala isn't really trying to become more dynamic, but it has a feature for dealing with problems that are dynamic anyway.
Erlang is reliable because it's fault tolerant. The Strong Static Typing camp wants software that is reliable because it is faultless.
Elixir has Erlang's philosophy on the problem. I think most of the wailing and gnashing of teeth is because most languages (even most statically typed ones historically) have just completely punted on the notion of language support for writing software that doesn't fall over in a stiff breeze. The more we build layers of software between humans and their actual goals the more this is going to come to a head.
And you are falling prey to the Nirvana fallacy [1].
Yes, we will never be able to prove that a program is 100% correct but that doesn't mean we shouldn't prefer solutions that bring that number up (statically typed languages) over solutions that don't (dynamically typed languages).
Just because you can't do something perfectly doesn't mean you shouldn't try to do it as best you can.
Yes. Real-world programming is an entirely different thing from academic research.
In the real world, it may well be the case that while you're screwing around with a baroque type system, your competition has iterated three or four times and your milkshake has been drunk.
Of course your compiler will never be able to proof the correctness (or lack of it) of all programs.
The relevant question is, what share of useful programs can our compilers help us creating? This is not answered yet, and you seem to have never even thought about it.
fun fact: the Busy Beaver function applied to the universe yields a finite number and seeing as we need to leave some space to actually run the program we can conclude that in fact any program that can be written can be proven to halt. Granted that in case of "for(;;){printf("hello");}" that halt is the heat death of the universe but it's still theoretically tractable.
