Are there any research projects trying to make "proof" programs / languages?

Dafny attempts to do something like this for imperative-style languages, using pre- and post-conditions: