> Is there a good language with the simplicity, portability, and control of C together with theorem-proving features? Yes: C ;-) The Frama-C system allows you

> Is there a good language with the simplicity, portability, and control of C together with theorem-proving features? Yes: C ;-) The Frama-C system allows you to write functional specifications of C code and verify them. Trivial example: http://frama-c.com/wp.html http://frama-c.com/wp.html It interfaces with the Why3 platform, which means that it can talk to dozens of automated provers out of the box. AFAIK it doesn't yet handle some things like dynamic allocation and free (the semantics of free in C is hard!), but it may be something you might want to play with.