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.
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.