[seL4] Joint a formally verified C compiler with seL4?

2 Mar 2015

      Hi all,

I've heard a formally verified optimizing C compiler: CompCert recently:
http://www.absint.com/compcert/ HN:
https://news.ycombinator.com/item?id=9130934 .

So what benefit will there be if some one use CompCert as the compiler for
seL4?

-- 
Cheers,
Grissiom