I have solved the halting problem. Every program you write compiles and executes as HALT; and therefore it's possible to determine if a program halts! It might not be correct but it sure is fast!
Many compiler writers are employed by hardware companies, and these companies are employing them to sell their hardware chips. For these companies, even a 1% boost in performance on $BENCHMARK can drive measurable impact on sales. Even if you're not worried about driving hardware sales, performance tends to be the major benchmark that gets mentioned in comparisons--note how the "Benchmarks Game" (what used to be called the Programming Language Shootout) compares languages solely on the basis of performance.
In other words, if you look at actual customer behavior, performance tends to be one of the most dominant factors in choosing one compiler over another (language compliance is probably more dominant, however). Surety of correctness is not a major factor at all.
Now, in order to actually report benchmarks correctly, you have to implement them correctly, so to some degree you have a basic guarantee that the compiler will usually work. But someone pointing out a soundness issue using a hypothetical example (as opposed to real code) is going to end up low priority because the evidence is that it doesn't matter in practice for the real, large applications that customers care about (as no one else has complained about it for the past several years).
In summary, practical performance will win out over theoretical correctness, but not practical correctness.
This is new to me (the Benchmarks Game has been around for well over a decade).
> 2) correctness is checked
This is par for the course of benchmarks. A benchmark that is incorrectly compiled provides no useful information whatsoever about performance. It's not really what people mean when they complain about correctness issues in the compiler (which is generally referred to as soundness in literature).
> 3) time "to complete and log all make actions" (build the program) is also logged
Performance in a compiler is usually taken to be a combination of runtime, code size, and compile time, although all three components are not weighted equally.
Or create OSes where applications are all written in managed languages, and the use of GCC and clang is gate keeped to the OS vendor and native libraries, just an idea.
Bit of a nitpick, but the real value is in safe languages, rather than managed languages, no? The distinction is a little blurry, admittedly, but as an example, I figure that verified SPARK counts as safe but unmanaged.
Still niche, Rust is not up to the stuff that app developers expect in terms of tooling and D still has quite a few @safe bugs to sort out, among its current adoption issues.
Unfortunely regardless of their own reports regarding CVEs, Microsoft, Apple and Google keep turning to C and C++ for their bottom layers + managed languages, instead of going full speed in some of those alternatives.
So it appears to be the long term solution to mitigate security issues, while keeping compatibility with existing code and tooling.
Frama-C is a specific compiler. It has not much to do with proving your own code. (And C ain't a good language for writing code you want to prove correct in.)
You are right that after having proven your code correct, you might want to use an implementation (compiler or interpreter), that is also proven correct. But those are still two different things.
I do; low level, OS and library code should be both. It's not an either or; you start with the correct code (and code to verify), then if needs be you optimize.
So you're saying maximum priority is correctness, and performance second place? Because if you don't have correctness you can't "start with correct code"
If you have a broken compiler, you can have broken generated code, and not even know it. This isn't about whether or not your C code is correct, this is about whether the assembly that's generated matches the behavior in your code.
Who cares how fast the code is, if it isn't the correct code?