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 lan

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 https://github.com/microsoft/Armada