OT: Have you looked at Ada SPARK 2014 yet? Provides nice and strong system programming language semantics. With a verification tool... nice. http://docs.adacore.com/spark2014-docs/html/ug/spark_2014.html