> Some day, I would like to design a language that gets this right. But for the moment, I remain focused on Sandstorm.io. Hopefully someone will beat me to it.

> Some day, I would like to design a language that gets this right. But for the moment, I remain focused on Sandstorm.io. Hopefully someone will beat me to it. Two language that do it: Whiley (http://whiley.org/ http://whiley.org/) and Dafny (http://rise4fun.com/dafny http://rise4fun.com/dafny). I expect (but not sure) that the proving power is about the same as what can be achieved by template meta-programming.