Armada

Even there it depends. 'Programming practices' is vague. Even C can be tamed, at great expense, using formal methods techniques. [0][1][2][3] Adoption of such methods can give a solid assurance of the lack of UB, like use of a safe language. Weaker measures, like adopting MISRA C, don't provide such strong assurances (although they can eliminate certain categories of errors), and as you indicate, their real value is a bit more subjective. Mandating a bad programming style could actively make things worse. [0] https://trust-in-soft.com/ [1] https://www.eschertech.com/products/perfect_developer.php [2] https://github.com/microsoft/Armada [3] https://www.microsoft.com/en-us/research/project/vcc-a-verif...

You're essentially describing a C compiler with advanced optimisations disabled, no? If you want improved safety and fewer footguns, the solution is to use a safer language than C, rather than to try to declaw a fundamentally unsafe language. Even MISRA C fails to guarantee the absence of undefined behaviour. (Other far more involved projects have made this a goal. [0][1]) The obvious candidates are Ada, Rust, and Zig. It doesn't make sense to mandate the absence of serious compiler optimisations, especially for a language like C. [0] https://github.com/zetzit/zz [1] https://github.com/microsoft/Armada

Thanks. I read Via a C-like language to mean their language compiles to a non-standard language resembling C, but as you say, they mean they defined a novel language that resembles C, and it compiles down to standard C (specifically, the C subset named ClightTSO suitable for use with the CompCertTSO compiler). Nowhere in Armada's overview [0] is it stated that the ultimate goal is to produce verified C code. I've heard of CompCert. Pity it hasn't got more traction. Also a pity about its licensing situation. The Free and Open Source community is not interested in semi-Free software. The DMD compiler showed us this. [0] https://github.com/microsoft/Armada

Perhaps worth noting is Armada https://github.com/microsoft/Armada which is built upon Dafny and targets a C-like language.