Metasepi has been discussed before here, but I haven’t seen FPIoT mentioned yet. The sheer geekiness of programming an Arduino with ATS makes me giddy
It’s a cool project. They need to remove the misinformation about C language they start with. Most safety-critical and rapidly-developed embedded are done in C language. Successfully. Astree Analyzer can also prove absence of all common errors in a subset. Frama-C and VCC can prove various properties. CompCert certifies the compilation. And so on.
They might say ATS is cheaper or requires less expertise to verify. Definitely on former but just a maybe on latter. So much tooling for C now such as AutoCorres.