3 ms·

A big problem is that proving that transformations preserve semantics is very hard. Formal methods has huge potential and I believe it will be a big part of the

A big problem is that proving that transformations preserve semantics is very hard. Formal methods has huge potential and I believe it will be a big part of the future, but it hasn't become mainstream yet. Probably a big reason why is that right now it's simply not practical: the things you can prove are much more limited than the things you can do, and it's a lot less work to just create a large testsuite. Example: CompCert (https://compcert.org/ https://compcert.org/), a formally-verified compiler AKA formally-verified sequence of semantics-preserving transformations from C code to Assembly. It's a great accomplishment, but few people are actually compiling their code with CompCert. Because GCC and LLVM are much faster[1], and have been used so widely that >99.9% of code is going to be compiled correctly, especially code which isn't doing anything extremely weird. But no matter how large a testsuite, how many tools like these exist, there may always be bugs. Formal verification provides guarantees that tests can't, and as we start relying on software more it will become more important. [1] From CompCert, "Performance of the generated code is decent but not outstanding: on PowerPC, about 90% of the performance of GCC version 4 at optimization level 1"

pfdietz 3y ago
If I understand correctly, CompCert doesn't promise to compile correct programs correctly. Rather, it promises that if the compile succeeds, it's correct. This means it suffices to have (for example) a proved-correct check that a coloring register allocator allocated correctly, but that's allowed to abort if the coloring is incorrect. The register allocator itself need not be proved correct. In practice, this is probably fine, since you won't run into bugs where the compiler aborts very often (and if you do, you know that you did.)

pfdietz 3y ago

If I understand correctly, CompCert doesn't promise to compile correct programs correctly. Rather, it promises that if the compile succeeds, it's correct. This means it suffices to have (for example) a proved-correct check that a coloring register allocator allocated correctly, but that's allowed to abort if the coloring is incorrect. The register allocator itself need not be proved correct. In practice, this is probably fine, since you won't run into bugs where the compiler aborts very often (and if you do, you know that you did.)