[dragontamer]

Take for example, proper use of a unique_ptr<lock_guard<std::mutex> > in C++. You can pass around the unique_ptr, and guarantee that you are in "unique ownership" of a particular lock at compile-time.

In C++, you may not be able to prove "the lack of race conditions", but you can prove things like "I'm the only one who is holding onto this mutex right now" thanks to stuff like unique_ptr... which tracks that stuff. These primitive proofs are performed at compiletime, and have little-to-no effect on runtime as well.

Stronger languages with stronger type-systems (ie: Haskell) can prove / disprove which code has side-effects... because you've explicitly passed the Monad around. (Note: Code without side-effects is guaranteed to not have race conditions).

So yes, there are important things you can prove using the type-system. More importantly, it is the compiler's job to automatically conduct these proofs every compile cycle.