I like this very much. For all the talk of power in languages, we make lots of mistakes. One underlooked decision factor in choosing languages should be, "How hard is to make accidental mistakes?" and "How easy is it to find and fix mistakes?"
One of the historical guidelines in C was "trust the programmer". This would be fine were it not for the fact that programmers, like all humans, are frail and fallible beings. Experience shows that whatever techniques are used it is hard to write "correct" software. It is good advice therefore to use tools that can help by finding bugs and preventing bugs. Ada was specifically designed to help in this respect."
https://www.adacore.com/adaanswers/gems/gem-30/
(And if even Ada is not restrictive enough, one uses Ada's subset Spark, e.g., http://www.spark-2014.org/ )
Not to say that one should use Ada (though it would often help I guess), but this different approach to software design and maintenance ("Ada culture"[1]) is worth knowing.
[1] http://archive.adaic.com/intro/ada-vs-c/ada-vs-c.html
My personal rule of thumb:
C and Scheme for explorative hacking, Ada and Haskell for reliable implementation, Perl for teh recreational lulz.
And it is a huge failure. No amount of runtime checks can make your already compiled and deployed program less wrong.
> (Taken from the Ada vs C++ comparison article) "Stroustrup (...) presents a use-defined vector class (...) Unfortunately, the proper implementation of the class requires exceptions (...)"
A proper implementation of the class requires dependent types. Runtime index checks are effectively testing, which can show the presence of bugs, but never their absence.
Sure, accidental mistakes are avoidable. But I don't think there is a way for the language to help us write proper abstractions. I mean if one doesn't know how to take mutable state from a bunch of functions and abstract its mutation away, i.e. allow it to mutate inside a single function only, than what can the language do? But what if you simply have an inconsistent code, like handling errors differently in different places?
Would you use a language that produces a warning of a hypothetical bug if you have state changes too far away from each other?
I'm not exactly sure what the solution is, but if history is any indication, these linguistic systems are often considered foul-proof to the point that those managing them stop managing them, or hand off management to someone and forget about it, letting any issue outside the scope of the language become a cancer of sorts that eventually kills the host.
I do think it's reasonable to have technical environments where language choices are done for support and debugging purposes, with the highest powered tools only pulled out on occasion.
Sadly, this is not true for us programmers. By and at large, we have preferred to devise mechanisms (such as exceptions and contracts) that protect us from the consequences of our mistakes, rather than attacking the root cause of these mistakes - our failure to enforce pre- and postconditions using static techniques. And this situation is not going to improve as long as we stick to a limited vision that embraces integers, strings, lists and trees, but not equality of terms as types.
Hell, this goes so far as to how we currently give people directions to cross a state. Consider http://goo.gl/maps/4F89Z This clearly doesn't work because there is not a car that can do that trip completely non-stop (well, that I know of). Yet, it would be silly to even try and account for all of the random stops that a person making that trip would want to do. How is this the fault of "embracing integers, strings, lists and trees?"
Having looked over all of the various ways that we give directions to kids lately, I'm becoming more and more convinced that the higher theories of programming are missing something (for a great presentation on this idea, see [1]). Look at how music is written. Look at how lego directions are written. Ikea directions. Shampoo directions. Cooking recipes. All of these are relatively successful methods for communicating often complicated sets of directions. None of them necessarily encode things to the level of detail that our programs require.
Are you concerned that all of my examples are not necessarily life and death detail oriented? See the blueprints of rockets. Sail boat designs from ancient times. Heck, sailing routes.
If anything, I would say that our programs should, instead of offering fancy ways to escape the consequences, programs should offer ways to "get back on the desired path" of what was supposed to be accomplished. The canonical "FileNotFound?" Don't put my program somewhere where I have to somehow set things back up to try again. Resume right here once the file has been found. (Sadly, I don't have any good thoughts on this. Just late night ramblings.)
[1] http://www.infoq.com/presentations/We-Really-Dont-Know-How-T...