Readit NewsAfter exchanging them on a bank into useful money: the average Euro coin weights about 3.6 grams and has an average value of 7 cents. :-)
Get rid if the source-files and put every function/method in its own "editor". However, as far as I remember navigation to/from callers was not possible in Smalltalk.
So CompCert seems to me to aim to help mission-critical software to move away from C, and possibly into Coq/Isabelle/etc., except for the purposes of compilation to machine code.
Thats my understanding too. Code is written in high level systems generating C as output. C becomes rather an implementation detail in a hopefully, more or less completely verified tool chain.
Curious why the author words it like this, rather than just "not supported".
This is used by compcert: https://compcert.org/
My question was whether it can help detecting translation errors from the first step.
If one wanted to criticize OCaml syntax, the need for .mli-files (with different syntax for function signatures) and the rather clunky module/signature syntax would be better candidates.