I’ve long wanted to develop compilers with techniques like this. I wish I understood it. :)
What is an incorrect compiler? Does this just mean no compiler bugs? Compiler bugs are not the problem with my software - I am the problem 99.999% of the time.
What is an incorrect compiler?
A compiler that generates an output not respecting the language’s specification.
I am the problem 99.999% of the time
Sure, but what do you do if the bug is in the compiler? Nothing. That’s why you want to know that the compiler you use is as close as possible to being bug-free.
Sure, but what do you do if the bug is in the compiler?
On the rare occasion that I even notice this situation, I rewrite my code in a way that doesn’t cause the compiler to have a bug. Similar to when a library that I use has a bug, so I work around it (if I don’t have easy access to the source of the library).
I still think the bigger problem is that the compiler may be taking my source code and outputting correct executable code, but the input source is wrong. “Correct” or “not correct” makes no difference – the output will not what I want. More than likely (very, very likely), I’ve written source code that compiles to the wrong thing (aka a bug).
I agree with you in that the bugs in a programs comes most of the time from its programmer and not he compiler. But btw, if one day I update my compiler and it creates code behaving the wrong way, it would be pretty bad as I might not notice it right away. So compiler verification is a pretty important topic I think.
Don’t get me wrong: I think it’s cool. I’m really trying to understand the benefit.
But btw, if one day I update my compiler and it creates code behaving the wrong way
Won’t the fact that you updated the compiler change the verification, since the verification is generated by creating the compiler? Isn’t the verification just verifying that the compiler does what it is supposed to? Will you know your code is behaving the wrong way?
To clarify, for example, many gcc optimizations are incorrect, although it’s mostly only Linus who diagnoses that. :)
I write Scala, so compiler bugs cause me a lot of pain.