Absolutely agree. Compcert solves a very difficult problem better than pretty much any other solution. However, that problem is mostly a theoretical one, even

Absolutely agree. Compcert solves a very difficult problem better than pretty much any other solution. However, that problem is mostly a theoretical one, even if it's important to mitigate it. It's not a replacement for source level verification and migrating the compiler can be put off until relatively late in a project.