C++ is no issue but, to make very small binaries packed with the features we need, you need a lot of fiddling and the end it does not look like c++. Not to ment

C++ is no issue but, to make very small binaries packed with the features we need, you need a lot of fiddling and the end it does not look like c++. Not to mention that most embedded devs (at least in Asian, Africa and eu embedded corps which make deployments of millions of mcu's, not home arduino users: there might be more of those) work mostly with C. I think most are waiting to skip a revolution to something like Rust but that does not fit yet. So this solution gives at least some handles to add verification. That said, there are more of these projects. I think there is an F* project too. > why would another language compiled to C be any better? It just doesn't make sense to me. It seems that the formalization in the article allows for very low level operation which you would use in C while not writing C. As said, sure you can do that in C++ but then you gain little or nothing. I have not tried this, only posted it because I would like for something robust like it to exist. Now we use Coq (or more recent idris) to write things and hand translate them to mcu asm/c.