> But, what would be your design criteria for the new language? I'd aim for somewhere between Rust and <other_imperitive_languages>. I'm certainly not qualifi

> But, what would be your design criteria for the new language? 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. Something like C, but with markup describing data lifetimes, value ranges, permissible access, etc. The guys at Bungie did something similar for Destiny: https://www.youtube.com/watch?v=v2Q_zHG3vqg&t=2791s https://www.youtube.com/watch?v=v2Q_zHG3vqg&t=2791s There are also some PHd folks working on adding type annotations to C and restricting aliasing rules. Those annotations/rules get fed through a solver that proves it's free of latent memory bugs. As far as I remember they're trying to prove the Android thread scheduler. I couldn't find the talk/slides, but it turns out that's hard in C, but with a brand new language you could probably do it pretty easily (easily being a few man-years, instead of tens of).