The problem with generated code is that it is rarely easy to understand or maintain. Suppose you need to add new features or fix a bug, to do so you will need all of the original specifications and code generation tools. Will those tools work on other platforms? Do they support all of the low level needs of C? For example, do they support bit-level layout for structs or inline assembly?
I believe that Rust will make more inroads to replace C in many domains. This will eliminate many of C's known issues that Certified Program Synthesis seeks to address.
If you need formal verification or proofs, SPARK https://en.wikipedia.org/wiki/SPARK_(programming_language) is a mature and effective tool with a proven track record. It lets developers write code that is easy to understand and maintain compared to generated code and can formally prove the correctness of programs.
C developers keep doing bad things. Using terse variable names, rolling their own general-purpose linked-lists and other algorithm primitives. So attacking the problem with automated code generation is nice, but will C developers, who keep making bad life choices, actually use it?
I believe that Rust will make more inroads to replace C in many domains. This will eliminate many of C's known issues that Certified Program Synthesis seeks to address.
If you need formal verification or proofs, SPARK https://en.wikipedia.org/wiki/SPARK_(programming_language) is a mature and effective tool with a proven track record. It lets developers write code that is easy to understand and maintain compared to generated code and can formally prove the correctness of programs.