>> I'd aim for somewhere between Rust and <other_imperitive_languages>. >> I'm certainly not qualified to speak with any authority on the matter of provably co

>> I'd aim for somewhere between Rust and <other_imperitive_languages>. >> I'm certainly not qualified to speak with any authority on the matter of provably correct programs, but it seems to me there's a middle ground there that has yet to get a lot of attention. For "provably correct programs", the "<other_imperative_language>" could be SPARK: https://learn.adacore.com/courses/intro-to-spark/chapters/01_Overview.html https://learn.adacore.com/courses/intro-to-spark/chapters/01... If you wait a bit, Ferrocene may be what you are looking for: https://ferroussystems.com/ferrocene/ https://ferroussystems.com/ferrocene/