[nickpsecurity]

No, it's still hard. The best approach I've seen to this outside CompCert is a project that independently tried my own recommendation of breaking it into stages then using whatever verification works on a per stage basis. So, one prover and approach works best for Stage 1. Then another maybe for Stage 2. Some compositional method to tie them together.

They were making a MIPS compiler. Got pretty far in short time paper covered with a fraction of CompCert's effort. Nonetheless, the untrusted compiler plus trusted checker method has the most supporting evidence in literature for getting the job done and ease of building. So, even my recommendation should take that approach where possible.

[Ericson2314]

It's hard, but I've for awhile thought that developing these tools in a more bottom-up would help. And of course orthogonal components, as you say, is a good idea for just about anything.

[nickpsecurity]

I don't agree. Matter of fact, I recommended it here in an answer to the reproducible build meme that pops up. See my conversation with jeffreyrogers here:

https://news.ycombinator.com/item?id=10182282

[nickpsecurity]

Looking back at it, I meant to say "I don't disagree. I had made similar recommendations before."

Totally changes meaning of comment till you click the link haha.