What kinds of programming pitfalls modern languages are able to find?

I often see claims that modern functional strictly-typed languages are 'safer' than others. These statement mostly linked with type systems and their ability to explicitly express the following pitfalls:

• Alternatives in function result. Maybe and Either datatypes vs. exceptions and null-pointers in C++-like languages.
• Access to mutable state (possibly inconsistent behavior over time). State datatype in Haskell vs. variables in C++-like languages.
• Performing IO. IO datatype in Haskell vs. just doing things in C++-like languages.

Haskell allows to express constraints required for safe handling of these situations. And compiler is able to warn programmer when he doesn't follow them.

Although pitfalls above are definitely the most common ones I can think of much more, for example:

• Unexpected resource consumption. Memory, CPU, disk, bandwidth.
• Inconsistent access to shared resources. Like read and write interference, broken lock ordering.
• System-level failure. Like crashing process or pulled plugs.
• Unexpected execution time for IO, timing violation.

Is there languages, libraries or at least models which allow to express constraints from the second set and yield a warning when they are not met?

• Jun 18, 2013 at 17:54
• I do not even understand the question. Are talking about detection of potential or actual problems ? Is it to be done at compile time or at run time ?... Jun 19, 2013 at 13:31
• I do not understand the question either. A Java-style "PrinterOutOfPaperException" could be construed as "requiring the programmer to handle a system failure." Jun 19, 2013 at 20:43
• @babou I'm talking about compile time. Not sure how do you distinguish potential problems from actual. If something bad could happen it will eventually happen :) Jun 20, 2013 at 12:03
• @JamesKoppel No, they only allow to ensure that we have some code block to execute in case of particular exception thrown. What I meant in the second case is ability to say if procedure 'a' maintains the system in recoverable state and procedure 'b' uses it in some "right" way than system is recoverable during entire 'b' execution. Jun 20, 2013 at 12:04

As something on the more extreme end, there is $\lambda_{\text{zap}}$, a typed lambda calculus designed to handle transient hardware faults e.g. cosmic rays. It is described in Static Typing for a Faulty Lambda Calculus by Walker et al.