[kazinator]

> then you are sure your program compiled with CompCert will result in a bug-free program.

That is simply not true. A UB-free program which calculates e is incorrect, if the task was to calculate pi. Anything downstream from that program which uses its output as if it were pi is going to break.

Correctness is only with respect to a specification.

Specifications can have issues. Aside from being vague or contradictory, they can neglect to include important requirements, such as being completely silent on the treatment of bad inputs. A program with an exploitable security flaw outside of its intended operation can in fact be correct, because those inputs lie outside of its requirements: i.e. just like a compiler, the program has its own undefined behaviors. Also, the requirements for a program can explicitly call for undefined behavior, like "divide a number by zero to demonstrate/test the platform-specific handling of the situation".

Calling a function outside of ISO C that is not defined in the C program itself is also undefined behavior, so these proven programs cannot use any platform libraries without relaxing what "undefined behavior" means.

[angry_octet]

That is a super pedantic nit picking response. You well knew what was meant. Everyone here knows the meaning of V&V.